Theorem eqeq1d 2186

Description: Deduction from equality to equivalence of equalities. (Contributed by NM, 27-Dec-1993.)

Hypothesis

Ref	Expression
eqeq1d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
eqeq1d	|- ( ph -> ( A = C <-> B = C ) )

Proof of Theorem eqeq1d

Step	Hyp	Ref	Expression
1		eqeq1d.1	. 2 |- ( ph -> A = B )
2		eqeq1 2184	. 2 |- ( A = B -> ( A = C <-> B = C ) )
3	1, 2	syl 14	1 |- ( ph -> ( A = C <-> B = C ) )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170

This theorem is referenced by:  rspcedeq1vd  2850  sbceq2g  3079  csbhypf  3095  csbiebt  3096  csbiebg  3099  dfss4st  3368  disjssun  3486  sneqrg  3761  preq12b  3769  preq12bg  3772  disji2  3994  iin0r  4167  opthg  4236  opeqsn  4250  unisucg  4412  opthreg  4553  tfisi  4584  dmsnopg  5097  relcoi1  5157  iotaeq  5183  iotabi  5184  fneq1  5301  fnun  5319  fnresdisj  5323  fnimadisj  5333  fnimaeq0  5334  sbcfng  5360  foeq1  5431  foco  5445  fveqeq2d  5520  fvelimab  5569  fvun1  5579  fvmptdv2  5602  fneqeql  5621  dffo3  5660  fvsng  5709  fconstfvm  5731  eufnfv  5743  f1veqaeq  5765  dff13f  5766  f1elima  5769  foeqcnvco  5786  f1eqcocnv  5787  acexmidlemab  5864  ovanraleqv  5894  eloprabga  5957  ovmpodv2  6003  ovi3  6006  ovelimab  6020  caovcang  6031  caovcan  6034  caovimo  6063  suppssfv  6074  suppssov1  6075  caofinvl  6100  op1stg  6146  op2ndg  6147  eqop  6173  reldm  6182  xporderlem  6227  tposfo2  6263  frec0g  6393  freccllem  6398  frecfcllem  6400  frecsuclem  6402  frecsuc  6403  nnm0r  6475  nnmord  6513  nnaordex  6524  nnawordex  6525  ereq1  6537  eqerlem  6561  mapsn  6685  endisj  6819  xpf1o  6839  mapxpen  6843  fidifsnen  6865  supelti  6996  updjudhcoinlf  7074  updjudhcoinrg  7075  updjud  7076  omp1eomlem  7088  difinfsnlem  7093  nnnninfeq  7121  enomnilem  7131  finomni  7133  exmidomni  7135  fodjuomnilemres  7141  fodjuomni  7142  ismkvnex  7148  mkvprop  7151  fodjumkvlemres  7152  enmkvlem  7154  enwomnilem  7162  nninfdcinf  7164  nninfwlporlem  7166  nninfwlpoimlemginf  7169  pm54.43  7184  exmidfodomrlemrALT  7197  cc2lem  7260  addnidpig  7330  ltexpi  7331  dfplpq2  7348  dfmpq2  7349  recexnq  7384  recmulnqg  7385  ltexnqq  7402  halfnqq  7404  enq0tr  7428  nqnq0pi  7432  addnnnq0  7443  addlocpr  7530  ltexprlemru  7606  ltexpri  7607  lteupri  7611  prplnqu  7614  recexpr  7632  addsrpr  7739  mulsrpr  7740  00sr  7763  negexsr  7766  recexgt0sr  7767  srpospr  7777  prsrriota  7782  caucvgsrlemfv  7785  map2psrprg  7799  elrealeu  7823  axrnegex  7873  axprecex  7874  rereceu  7883  recriota  7884  nntopi  7888  axcaucvglemval  7891  axcaucvglemcau  7892  cnegexlem1  8126  cnegex  8129  cnegex2  8130  subval  8143  subadd  8154  subadd2  8155  subsub23  8156  addsubeq4  8166  subcan2  8176  negcon1  8203  subcan  8206  addrsub  8322  ltadd2  8370  ltordlem  8433  recexre  8529  recexap  8604  muleqadd  8619  receuap  8620  divvalap  8625  divmulap  8626  rec11ap  8661  rerecapb  8794  zdiv  9335  uzin  9554  xaddval  9839  xnn0xadd0  9861  xnegdi  9862  xltadd1  9870  icc0r  9920  fznlem  10034  fseq1m1p1  10088  1fv  10132  fzon  10159  fvinim0ffz  10234  ioo0  10253  ico0  10255  ioc0  10256  flqbi  10283  divfl0  10289  modq0  10322  modqmuladdnn0  10361  addmodlteq  10391  frecuzrdgtcl  10405  frecuzrdgfunlem  10412  seq3f1olemstep  10494  seq3f1olemp  10495  seq3id  10501  seq3z  10504  qsqeqor  10623  mulreap  10864  rennim  11002  resqrexlemex  11025  rsqrmo  11027  resqrtcl  11029  rersqrtthlem  11030  sqrtsq2  11043  isumss  11390  fsum00  11461  telfsumo  11465  pwm1geoserap1  11507  prodssdc  11588  absefib  11769  efieq1re  11770  divides  11787  dvdsval2  11788  nndivides  11795  dvds0lem  11799  dvds1lem  11800  dvds2lem  11801  negdvdsb  11805  muldvds1  11814  muldvds2  11815  dvdscmulr  11818  dvdsmulcr  11819  dvdstr  11826  dvdsabseq  11843  divconjdvds  11845  odd2np1lem  11867  odd2np1  11868  even2n  11869  oddm1even  11870  2tp1odd  11879  opeo  11892  omeo  11893  m1exp1  11896  divalgb  11920  gcdaddm  11975  gcdabs1  11980  bezout  12002  gcdmultiple  12011  gcdmultiplez  12012  rplpwr  12018  rppwr  12019  alginv  12037  algcvga  12041  algfx  12042  eucalgval2  12043  coprmdvds  12082  qredeq  12086  qredeu  12087  divgcdcoprm0  12091  divgcdcoprmex  12092  cncongr1  12093  rpexp  12143  rpexp12i  12145  cncongrprm  12147  qnumdenbi  12182  phival  12203  phicl2  12204  dfphi2  12210  phiprmpw  12212  phimullem  12215  eulerthlem1  12217  eulerthlemfi  12218  eulerthlemrprm  12219  eulerthlemth  12222  eulerth  12223  fermltl  12224  hashgcdlem  12228  phisum  12230  odzval  12231  odzdvds  12235  reumodprminv  12243  modprm0  12244  nnnn0modprm0  12245  modprmn0modprm0  12246  coprimeprodsq  12247  coprimeprodsq2  12248  pythagtriplem2  12256  pythagtrip  12273  pceulem  12284  pcval  12286  pcqmul  12293  pcqcl  12296  pcabs  12315  pc2dvds  12319  pcaddlem  12328  pcadd  12329  pcmpt  12331  prmpwdvds  12343  pockthi  12346  ennnfonelemhf1o  12404  mgmidmo  12721  grpidvalg  12722  grpidpropdg  12723  ismgmid  12726  ismgmid2  12729  mgmidsssn0  12733  grprinvlem  12734  grpridd  12736  ismnddef  12749  sgrpidmndm  12751  ismndd  12768  mndpropd  12771  mndinvmod  12774  mnd1  12775  ismhm  12781  grpinvex  12815  isgrpd2  12825  isgrpd  12827  dfgrp2  12830  grpinveu  12839  grpinvval  12844  grplinv  12850  isgrpinv  12854  grplrinv  12855  grpidinv2  12856  grpidinv  12857  grplmulf1o  12872  grpsubeq0  12884  grpsubadd  12886  dfgrp3mlem  12896  dfgrp3m  12897  grp1  12904  mhmmnd  12908  ghmgrp  12910  mulgval  12914  mulgaddcom  12934  ablsubadd  13015  ablsubsub23  13028  dfur2g  13045  srgideu  13055  srgidmlem  13061  issrgid  13064  srgrz  13067  srglz  13068  srgisid  13069  srg1zr  13070  ringideu  13100  ringidmlem  13105  isringid  13108  ringid  13109  oppr0g  13150  oppr1g  13151  reldvdsrsrg  13160  dvdsrvald  13161  dvdsrmuld  13164  dvdsr01  13172  dvdsr02  13173  opprunitd  13178  crngunit  13179  unitinvinv  13192  dvreq1  13210  dvdsrpropdg  13215  lringuplu  13236  ntreq0  13414  ispsmet  13605  psmet0  13609  ismet  13626  isxmet  13627  xmeteq0  13641  metn0  13660  xmetres2  13661  xblss2ps  13686  xblss2  13687  xmseq0  13750  comet  13781  bdxmet  13783  cnmet  13812  ivthdec  13904  reeff1o  13976  ioocosf1o  14057  logbgcd1irr  14167  logbgcd1irraplemexp  14168  lgsval  14187  lgsdir  14218  lgsne0  14221  lgsprme0  14225  lgsdirnn0  14230  2sqlem7  14239  2sqlem8  14241  2sqlem9  14242  bj-charfunbi  14334  pwle2  14519  subctctexmid  14521  peano4nninf  14526  nninfalllem1  14528  nninfsellemdc  14530  nninfsellemeq  14534  nninfsellemqall  14535  nninfsellemeqinf  14536  isomninnlem  14549  trilpolemlt1  14560  trirec0  14563  iswomninnlem  14568  iswomni0  14570  ismkvnnlem  14571  dceqnconst  14578  dcapnconst  14579