Theorem eqeq1d 2214

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 2212	. 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 1373

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  rspcedeq1vd  2886  sbceq2g  3115  csbhypf  3132  csbiebt  3133  csbiebg  3136  dfss4st  3406  disjssun  3524  sneqrg  3803  preq12b  3811  preq12bg  3814  disji2  4037  invdisjrab  4039  iin0r  4214  opthg  4283  opeqsn  4298  unisucg  4462  opthreg  4605  tfisi  4636  dmsnopg  5155  relcoi1  5215  iotaeq  5241  iotabi  5242  fneq1  5363  fnun  5383  fnresdisj  5387  fnimadisj  5398  fnimaeq0  5399  sbcfng  5425  foeq1  5496  foco  5511  fveqeq2d  5586  fvelimab  5637  fvun1  5647  fvmptdv2  5671  fneqeql  5690  dffo3  5729  fvsng  5782  fconstfvm  5804  eufnfv  5817  f1veqaeq  5840  dff13f  5841  f1elima  5844  foeqcnvco  5861  f1eqcocnv  5862  acexmidlemab  5940  ovanraleqv  5970  eloprabga  6034  ovmpodv2  6081  ovi3  6085  ovelimab  6099  caovcang  6110  caovcan  6113  caovimo  6142  suppssfv  6156  suppssov1  6157  caofinvl  6186  caofid1  6189  caofid2  6190  uchoice  6225  op1stg  6238  op2ndg  6239  eqop  6265  reldm  6274  xporderlem  6319  tposfo2  6355  frec0g  6485  freccllem  6490  frecfcllem  6492  frecsuclem  6494  frecsuc  6495  nnm0r  6567  nnmord  6605  nnaordex  6616  nnawordex  6617  ereq1  6629  eqerlem  6653  mapsn  6779  endisj  6921  pw2f1odclem  6933  xpf1o  6943  mapxpen  6947  fidifsnen  6969  supelti  7106  updjudhcoinlf  7184  updjudhcoinrg  7185  updjud  7186  omp1eomlem  7198  difinfsnlem  7203  nnnninfeq  7232  enomnilem  7242  finomni  7244  exmidomni  7246  fodjuomnilemres  7252  fodjuomni  7253  ismkvnex  7259  mkvprop  7262  fodjumkvlemres  7263  enmkvlem  7265  enwomnilem  7273  nninfdcinf  7275  nninfwlporlem  7277  nninfwlpoimlemginf  7280  pm54.43  7300  exmidfodomrlemrALT  7313  cc2lem  7380  addnidpig  7451  ltexpi  7452  dfplpq2  7469  dfmpq2  7470  recexnq  7505  recmulnqg  7506  ltexnqq  7523  halfnqq  7525  enq0tr  7549  nqnq0pi  7553  addnnnq0  7564  addlocpr  7651  ltexprlemru  7727  ltexpri  7728  lteupri  7732  prplnqu  7735  recexpr  7753  addsrpr  7860  mulsrpr  7861  00sr  7884  negexsr  7887  recexgt0sr  7888  srpospr  7898  prsrriota  7903  caucvgsrlemfv  7906  map2psrprg  7920  elrealeu  7944  axrnegex  7994  axprecex  7995  rereceu  8004  recriota  8005  nntopi  8009  axcaucvglemval  8012  axcaucvglemcau  8013  cnegexlem1  8249  cnegex  8252  cnegex2  8253  subval  8266  subadd  8277  subadd2  8278  subsub23  8279  addsubeq4  8289  subcan2  8299  negcon1  8326  subcan  8329  addrsub  8445  ltadd2  8494  ltordlem  8557  recexre  8653  recexap  8728  muleqadd  8743  receuap  8744  divvalap  8749  divmulap  8750  rec11ap  8785  rerecapb  8918  zdiv  9463  uzin  9683  xaddval  9969  xnn0xadd0  9991  xnegdi  9992  xltadd1  10000  icc0r  10050  fznlem  10165  fseq1m1p1  10219  1fv  10263  fzon  10291  fvinim0ffz  10372  ioo0  10404  ico0  10406  ioc0  10407  flqbi  10435  divfl0  10441  modq0  10476  modqmuladdnn0  10515  addmodlteq  10545  frecuzrdgtcl  10559  frecuzrdgfunlem  10566  seq3f1olemstep  10661  seq3f1olemp  10662  seq3id  10672  seq3z  10675  qsqeqor  10797  ccat0  11055  wrdl1s1  11087  ccatws1lenp1bg  11092  pfxsuff1eqwrdeq  11153  mulreap  11208  rennim  11346  resqrexlemex  11369  rsqrmo  11371  resqrtcl  11373  rersqrtthlem  11374  sqrtsq2  11387  isumss  11735  fsum00  11806  telfsumo  11810  pwm1geoserap1  11852  prodssdc  11933  absefib  12115  efieq1re  12116  divides  12133  dvdsval2  12134  nndivides  12141  dvds0lem  12145  dvds1lem  12146  dvds2lem  12147  negdvdsb  12151  muldvds1  12160  muldvds2  12161  dvdscmulr  12164  dvdsmulcr  12165  dvdstr  12172  dvdsabseq  12191  divconjdvds  12193  odd2np1lem  12216  odd2np1  12217  even2n  12218  oddm1even  12219  2tp1odd  12228  opeo  12241  omeo  12242  m1exp1  12245  divalgb  12269  gcdaddm  12338  gcdabs1  12343  bezout  12365  gcdmultiple  12374  gcdmultiplez  12375  rplpwr  12381  rppwr  12382  nninfctlemfo  12394  alginv  12402  algcvga  12406  algfx  12407  eucalgval2  12408  coprmdvds  12447  qredeq  12451  qredeu  12452  divgcdcoprm0  12456  divgcdcoprmex  12457  cncongr1  12458  rpexp  12508  rpexp12i  12510  cncongrprm  12512  qnumdenbi  12547  phival  12568  phicl2  12569  dfphi2  12575  phiprmpw  12577  phimullem  12580  eulerthlem1  12582  eulerthlemfi  12583  eulerthlemrprm  12584  eulerthlemth  12587  eulerth  12588  fermltl  12589  hashgcdlem  12593  phisum  12596  odzval  12597  odzdvds  12601  reumodprminv  12609  modprm0  12610  nnnn0modprm0  12611  modprmn0modprm0  12612  coprimeprodsq  12613  coprimeprodsq2  12614  pythagtriplem2  12622  pythagtrip  12639  pceulem  12650  pcval  12652  pcqmul  12659  pcqcl  12662  pcabs  12682  pc2dvds  12686  pcaddlem  12695  pcadd  12696  pcmpt  12699  prmpwdvds  12711  pockthi  12714  4sqlem12  12758  ennnfonelemhf1o  12817  fvprif  13208  mgmidmo  13237  grpidvalg  13238  grpidpropdg  13239  ismgmid  13242  ismgmid2  13245  mgmidsssn0  13249  grpinvalem  13250  grprida  13252  igsumvalx  13254  gsumress  13260  ismnddef  13283  sgrpidmndm  13285  ismndd  13302  mndpropd  13305  mndinvmod  13310  mnd1  13320  ismhm  13326  gsumvallem2  13358  grpinvex  13375  isgrpd2  13386  isgrpd  13388  dfgrp2  13392  grpinveu  13403  grpinvval  13408  grplinv  13415  isgrpinv  13419  grplrinv  13422  grpidinv2  13423  grpidinv  13424  grplmulf1o  13439  grpsubeq0  13451  grpsubadd  13453  dfgrp3mlem  13463  dfgrp3m  13464  grp1  13471  imasgrp2  13479  qusgrp2  13482  mhmmnd  13485  ghmgrp  13487  mulgval  13491  mulgaddcom  13515  eqg0el  13598  ghmeqker  13640  ghmf1  13642  conjnmzb  13649  ablsubadd  13681  ablsubsub23  13694  rngmneg1  13742  rngmneg2  13743  dfur2g  13757  srgideu  13767  srgidmlem  13773  issrgid  13776  srgrz  13779  srglz  13780  srgisid  13781  srg1zr  13782  ringideu  13812  ringidmlem  13817  isringid  13820  ringid  13821  qusring2  13861  oppr0g  13876  oppr1g  13877  reldvdsrsrg  13887  dvdsrvald  13888  dvdsrmuld  13891  dvdsr01  13899  dvdsr02  13900  opprunitd  13905  crngunit  13906  unitinvinv  13919  dvreq1  13937  dvdsrpropdg  13942  rhmdvdsr  13970  lringuplu  13991  subrg1  14026  subrgdvds  14030  isrrg  14058  rrgeq0i  14059  rrgeq0  14060  domneq0  14067  islmod  14086  islmodd  14088  lmodprop2d  14143  lss1d  14178  cnfldui  14384  znval  14431  znidom  14452  znunit  14454  znrrg  14455  mplelbascoe  14487  ntreq0  14637  ispsmet  14828  psmet0  14832  ismet  14849  isxmet  14850  xmeteq0  14864  metn0  14883  xmetres2  14884  xblss2ps  14909  xblss2  14910  xmseq0  14973  comet  15004  bdxmet  15006  cnmet  15035  ivthdec  15149  ivthreinc  15150  elply2  15240  reeff1o  15278  ioocosf1o  15359  logbgcd1irr  15472  logbgcd1irraplemexp  15473  mpodvdsmulf1o  15495  lgsval  15514  lgsdir  15545  lgsne0  15548  lgsprme0  15552  lgsdirnn0  15557  gausslemma2dlem0c  15561  gausslemma2dlem0i  15567  gausslemma2dlem7  15578  gausslemma2d  15579  lgseisenlem2  15581  lgseisenlem3  15582  lgsquadlem1  15587  lgsquadlem2  15588  lgsquad2lem2  15592  lgsquad3  15594  m1lgs  15595  2lgs  15614  2sqlem7  15631  2sqlem8  15633  2sqlem9  15634  edg0iedg0g  15693  bj-charfunbi  15784  2omap  15969  pwle2  15972  subctctexmid  15974  peano4nninf  15980  nninfalllem1  15982  nninfsellemdc  15984  nninfsellemeq  15988  nninfsellemqall  15989  nninfsellemeqinf  15990  isomninnlem  16006  trilpolemlt1  16017  trirec0  16020  iswomninnlem  16025  iswomni0  16027  ismkvnnlem  16028  dceqnconst  16036  dcapnconst  16037