HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem eqeq1d 1475
Description: Deduction from equality to equivalence of equalities.
Hypothesis
Ref Expression
eqeq1d.1 |- (ph -> A = B)
Assertion
Ref Expression
eqeq1d |- (ph -> (A = C <-> B = C))
Proof of Theorem eqeq1d
StepHypRef Expression
1 eqeq1d.1 . 2 |- (ph -> A = B)
2 eqeq1 1473 . 2 |- (A = B -> (A = C <-> B = C))
31, 2syl 10 1 |- (ph -> (A = C <-> B = C))
Colors of variables: wff set class
Syntax hints:   -> wi 3   <-> wb 146   = wceq 953
This theorem is referenced by:  eqeq12d 1481  sbceq2dig 2006  csbieb 2020  uniiunlem 2122  preq12b 2474  iin0 2730  opthgg 2779  opprc3 2787  opth2 2789  opeqsn 2791  frc 2910  frirr 2914  wefrc 2933  onfr 2976  nsuceq0 3043  fneq1 3568  fnun 3580  fnresdisj 3583  funimadisj 3592  foeq1 3653  foco 3667  fvprc 3706  fveq1 3708  fveq2 3709  fvres 3719  funbrfv 3735  fnbrfvb 3738  fvopabn 3771  elrnopabg 3785  dffo3 3804  fconstfv 3834  f1fvf 3860  f1fveq 3861  f1ocnvfv3 3868  isofrlem 3886  tz7.48lem 3940  tz7.49 3944  abianfplem 3946  caoprcan 4041  caoprmo 4056  op2ndg 4072  2ndconst 4081  elrnoprabg 4108  oe0m1 4144  om0r 4158  oe1m 4163  oawordeulem 4172  oawordeu 4173  omord 4183  oneo 4196  nneob 4239  erth 4266  mapsn 4329  endisj 4417  pw2en 4426  mapenlem2 4470  fodomfib 4541  pm54.43 4546  opthreg 4576  aceq5 4712  kmlem9 4745  zorn2lem7 4766  fodomb 4772  unxpdomlem 4815  cfeq0 4886  addnidpi 5000  ltexpi 5001  recmulpq 5042  dmrecpq 5046  ltexpq 5052  halfpq 5054  ltbtwnpq 5056  ltexpri 5121  recexpr 5132  00sr 5180  negexsr 5183  recexsrlem 5184  recexsr 5188  elreal 5222  axrnegex 5255  axrrecex 5256  cnegextlem1 5317  cnegext 5320  addcan 5323  addcant 5324  negeu 5327  subvalt 5329  subadd 5343  subaddt 5347  subsub23t 5348  subidt 5367  neg11t 5381  negcon1t 5382  mul01t 5415  add20 5576  recext 5657  mulcan 5659  mulcant2 5660  mul0ort 5665  muleqaddt 5669  receu 5670  divval 5673  divmul 5674  divmulz 5675  divmult 5676  divcan1z 5687  divcan2z 5688  divcan1t 5689  divcan2t 5690  divne0bt 5691  recidt 5698  divcan3z 5716  divcan3t 5718  div11t 5721  rec11 5734  rec11rt 5735  redivcl 5754  nndivt 5906  flbit 6184  ioo0t 6305  icoun 6346  1expt 6516  expeq0t 6517  sq0t 6550  sq11t 6560  sqeqort 6580  nn0opth2t 6598  sqr00t 6644  sqr2irrlem2 6655  sqr2irrlem3 6656  sqr2irrlem5 6658  crut 6668  replimt 6692  abs00t 6788  abs1m 6841  climconst3 7033  ivthlem9 7224  isupivth 7225  dsupivthlem 7226  efcltlem2 7247  ef0lem 7252  reeff1 7350  reeff1olem1 7364  reeff1olem1OLD 7366  reeff1o 7368  acdc3 7429  acdc5 7435  unbenlem 7447  ruclem37 7489  infxpidmlem11 7505  retopbas 7597  0ntr 7644  ntreq0 7650  ismet 7737  ismsg 7739  msflem 7742  meteq0 7751  metreslem 7762  metxp 7774  methausi 7820  cnmet 7843  blssioo 7852  dscmet 7856  bcthlem33 7965  bcth 7966  isgrp 7975  isgrpi 7976  grpidinvlem3 7984  grpideu 7987  grpidval 7992  grpidinv2 7994  grpinveu 7998  grpinvval 8001  grpinv 8003  isgrp2i 8011  cnid 8064  addinv 8065  mulid 8069  ghgrpilem3 8072  isring 8078  ringi 8079  cnring 8099  ringsn 8100  vci 8104  isvcgOLD 8133  isvclem 8134  isnvlem 8167  isnvgOLD 8168  nvi 8173  nvmul0or 8212  nvsubadd 8215  nvsubsub23 8222  nvz 8236  imsmetlem 8261  iporthcom 8303  ipz 8306  lnoval 8347  nmorepnf 8363  nmlno0i 8386  nmlno0 8387  ajfval 8400  hmoval 8401  isphg 8407  isph 8412  ip2eqi 8448  minveceu 8514  minvecdist 8516  pilem1 8590  pilem2 8591  pilem3 8592  pilem4 8593  sinperlem2 8606  cosh111t 8632  efif 8636  efifolem3 8639  efifolem6 8642  efifolem7 8643  efifo 8644  efif1lem6 8650  elcircOLD 8654  efielcirc 8659  circgrp 8660  effoi 8666  logeftb 8686  logeftbOLD 8706  hvmul0ort 8815  hvsubeq0t 8856  hvaddeq0t 8857  hvaddcant 8858  hvmulcant 8860  hvmulcan2t 8861  hvsubaddt 8865  his6t 8886  hial0 8889  hial02 8890  hi2eqt 8892  orthcom 8895  normlem7tALT 8906  normsub0t 8924  normpytht 8933  hilid 8949  norm1ex 9043  hhssnv 9054  ocelt 9070  ocsh 9072  ocorth 9080  ocin 9085  occllem5 9093  occllem8 9096  pjthlem13 9146  pjthlem14 9147  pjeq2t 9156  omls 9161  pjoc1t 9182  pjomlt 9184  pjoc2t 9187  choc0 9205  chm0t 9329  chocint 9333  chlejb1t 9350  chlejb2t 9351  chjot 9353  h1deot 9387  h1de2 9391  pjoml6 9449  pjoml2t 9471  pjoml3t 9472  pjcht 9556  pj11t 9576  hods 9618  hodidt 9635  eigortht 9681  nmoprepnf 9711  elunopt 9716  nmfnrepnf 9724  nlfnvalt 9725  adjvalt 9731  eigvecvalt 9739  unopf1ot 9756  elnlfnt 9768  adjt 9773  adjeqt 9775  hmdmadjt 9780  nmlnop0t 9838  lnopeq0 9847  lnopeq 9848  lnopeqt 9849  elunop2t 9853  lnfn0t 9891  riesz4 9911  riesz4t 9912  riesz1t 9913  cnlnadjlem3 9917  cnlnadjlem4 9918  cnlnadjlem5 9919  cnlnadjeut 9926  cnlnssadj 9928  adjbd1o 9933  nmopadjle 9936  hmopidmcht 9992  hmopidmpjt 9993  pjima 10015  pjhmopidm 10020  stelt 10051  hstelt 10052  hstel2t 10056  stadd3 10085  strlem1 10087  str 10094  hstr 10102  large 10104  golem2 10109  stcltr1 10111  superpos 10189  sumdmdi 10249  mddmdin0 10263  elghomlem1 10287  ghomgsg 10300  ghomf1olem 10301  cayleylem3 10318  erdisj2 10343  hmeogrp 10425  dtt2 10462  isded 10513  dedi 10514  cmppfd 10522  domcmpd 10523  codcmpd 10524  iscat 10531  cati 10532  cmpasso 10550  cmpida 10551  cmpidb 10552  ishoma 10559  ishomc 10561  ishomd 10562  ismonb2 10582  cmpmon 10585  isfuna 10592  isfunb 10593  ishgrag 10605  hgralem 10606  ispgrag 10615
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-ext 1452
This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1462
Copyright terms: Public domain