Theorem eqeq1d 2216

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 2214	. 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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2189

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

This theorem is referenced by:  rspcedeq1vd  2893  sbceq2g  3123  csbhypf  3140  csbiebt  3141  csbiebg  3144  dfss4st  3414  disjssun  3532  sneqrg  3816  preq12b  3824  preq12bg  3827  disji2  4051  invdisjrab  4053  iin0r  4229  opthg  4300  opeqsn  4315  unisucg  4479  opthreg  4622  tfisi  4653  dmsnopg  5173  relcoi1  5233  iotaeq  5259  iotabi  5260  fneq1  5381  fnun  5401  fnresdisj  5405  fnimadisj  5416  fnimaeq0  5417  sbcfng  5443  foeq1  5516  foco  5531  fveqeq2d  5607  fvelimab  5658  fvun1  5668  fvmptdv2  5692  fneqeql  5711  dffo3  5750  fvsng  5803  fconstfvm  5825  eufnfv  5838  f1veqaeq  5861  dff13f  5862  f1elima  5865  foeqcnvco  5882  f1eqcocnv  5883  acexmidlemab  5961  ovanraleqv  5991  eloprabga  6055  ovmpodv2  6102  ovi3  6106  ovelimab  6120  caovcang  6131  caovcan  6134  caovimo  6163  suppssfv  6177  suppssov1  6178  caofinvl  6207  caofid1  6210  caofid2  6211  uchoice  6246  op1stg  6259  op2ndg  6260  eqop  6286  reldm  6295  xporderlem  6340  tposfo2  6376  frec0g  6506  freccllem  6511  frecfcllem  6513  frecsuclem  6515  frecsuc  6516  nnm0r  6588  nnmord  6626  nnaordex  6637  nnawordex  6638  ereq1  6650  eqerlem  6674  mapsn  6800  endisj  6944  pw2f1odclem  6956  xpf1o  6966  mapxpen  6970  fidifsnen  6993  supelti  7130  updjudhcoinlf  7208  updjudhcoinrg  7209  updjud  7210  omp1eomlem  7222  difinfsnlem  7227  nnnninfeq  7256  enomnilem  7266  finomni  7268  exmidomni  7270  fodjuomnilemres  7276  fodjuomni  7277  ismkvnex  7283  mkvprop  7286  fodjumkvlemres  7287  enmkvlem  7289  enwomnilem  7297  nninfdcinf  7299  nninfwlporlem  7301  nninfwlpoimlemginf  7304  pm54.43  7324  exmidfodomrlemrALT  7342  cc2lem  7413  addnidpig  7484  ltexpi  7485  dfplpq2  7502  dfmpq2  7503  recexnq  7538  recmulnqg  7539  ltexnqq  7556  halfnqq  7558  enq0tr  7582  nqnq0pi  7586  addnnnq0  7597  addlocpr  7684  ltexprlemru  7760  ltexpri  7761  lteupri  7765  prplnqu  7768  recexpr  7786  addsrpr  7893  mulsrpr  7894  00sr  7917  negexsr  7920  recexgt0sr  7921  srpospr  7931  prsrriota  7936  caucvgsrlemfv  7939  map2psrprg  7953  elrealeu  7977  axrnegex  8027  axprecex  8028  rereceu  8037  recriota  8038  nntopi  8042  axcaucvglemval  8045  axcaucvglemcau  8046  cnegexlem1  8282  cnegex  8285  cnegex2  8286  subval  8299  subadd  8310  subadd2  8311  subsub23  8312  addsubeq4  8322  subcan2  8332  negcon1  8359  subcan  8362  addrsub  8478  ltadd2  8527  ltordlem  8590  recexre  8686  recexap  8761  muleqadd  8776  receuap  8777  divvalap  8782  divmulap  8783  rec11ap  8818  rerecapb  8951  zdiv  9496  uzin  9716  xaddval  10002  xnn0xadd0  10024  xnegdi  10025  xltadd1  10033  icc0r  10083  fznlem  10198  fseq1m1p1  10252  1fv  10296  fzon  10324  fvinim0ffz  10407  ioo0  10439  ico0  10441  ioc0  10442  flqbi  10470  divfl0  10476  modq0  10511  modqmuladdnn0  10550  addmodlteq  10580  frecuzrdgtcl  10594  frecuzrdgfunlem  10601  seq3f1olemstep  10696  seq3f1olemp  10697  seq3id  10707  seq3z  10710  qsqeqor  10832  ccat0  11090  wrdl1s1  11122  ccatws1lenp1bg  11127  pfxsuff1eqwrdeq  11190  swrdccatin2  11220  pfxccatin12lem2  11222  mulreap  11290  rennim  11428  resqrexlemex  11451  rsqrmo  11453  resqrtcl  11455  rersqrtthlem  11456  sqrtsq2  11469  isumss  11817  fsum00  11888  telfsumo  11892  pwm1geoserap1  11934  prodssdc  12015  absefib  12197  efieq1re  12198  divides  12215  dvdsval2  12216  nndivides  12223  dvds0lem  12227  dvds1lem  12228  dvds2lem  12229  negdvdsb  12233  muldvds1  12242  muldvds2  12243  dvdscmulr  12246  dvdsmulcr  12247  dvdstr  12254  dvdsabseq  12273  divconjdvds  12275  odd2np1lem  12298  odd2np1  12299  even2n  12300  oddm1even  12301  2tp1odd  12310  opeo  12323  omeo  12324  m1exp1  12327  divalgb  12351  gcdaddm  12420  gcdabs1  12425  bezout  12447  gcdmultiple  12456  gcdmultiplez  12457  rplpwr  12463  rppwr  12464  nninfctlemfo  12476  alginv  12484  algcvga  12488  algfx  12489  eucalgval2  12490  coprmdvds  12529  qredeq  12533  qredeu  12534  divgcdcoprm0  12538  divgcdcoprmex  12539  cncongr1  12540  rpexp  12590  rpexp12i  12592  cncongrprm  12594  qnumdenbi  12629  phival  12650  phicl2  12651  dfphi2  12657  phiprmpw  12659  phimullem  12662  eulerthlem1  12664  eulerthlemfi  12665  eulerthlemrprm  12666  eulerthlemth  12669  eulerth  12670  fermltl  12671  hashgcdlem  12675  phisum  12678  odzval  12679  odzdvds  12683  reumodprminv  12691  modprm0  12692  nnnn0modprm0  12693  modprmn0modprm0  12694  coprimeprodsq  12695  coprimeprodsq2  12696  pythagtriplem2  12704  pythagtrip  12721  pceulem  12732  pcval  12734  pcqmul  12741  pcqcl  12744  pcabs  12764  pc2dvds  12768  pcaddlem  12777  pcadd  12778  pcmpt  12781  prmpwdvds  12793  pockthi  12796  4sqlem12  12840  ennnfonelemhf1o  12899  fvprif  13290  mgmidmo  13319  grpidvalg  13320  grpidpropdg  13321  ismgmid  13324  ismgmid2  13327  mgmidsssn0  13331  grpinvalem  13332  grprida  13334  igsumvalx  13336  gsumress  13342  ismnddef  13365  sgrpidmndm  13367  ismndd  13384  mndpropd  13387  mndinvmod  13392  mnd1  13402  ismhm  13408  gsumvallem2  13440  grpinvex  13457  isgrpd2  13468  isgrpd  13470  dfgrp2  13474  grpinveu  13485  grpinvval  13490  grplinv  13497  isgrpinv  13501  grplrinv  13504  grpidinv2  13505  grpidinv  13506  grplmulf1o  13521  grpsubeq0  13533  grpsubadd  13535  dfgrp3mlem  13545  dfgrp3m  13546  grp1  13553  imasgrp2  13561  qusgrp2  13564  mhmmnd  13567  ghmgrp  13569  mulgval  13573  mulgaddcom  13597  eqg0el  13680  ghmeqker  13722  ghmf1  13724  conjnmzb  13731  ablsubadd  13763  ablsubsub23  13776  rngmneg1  13824  rngmneg2  13825  dfur2g  13839  srgideu  13849  srgidmlem  13855  issrgid  13858  srgrz  13861  srglz  13862  srgisid  13863  srg1zr  13864  ringideu  13894  ringidmlem  13899  isringid  13902  ringid  13903  qusring2  13943  oppr0g  13958  oppr1g  13959  reldvdsrsrg  13969  dvdsrvald  13970  dvdsrmuld  13973  dvdsr01  13981  dvdsr02  13982  opprunitd  13987  crngunit  13988  unitinvinv  14001  dvreq1  14019  dvdsrpropdg  14024  rhmdvdsr  14052  lringuplu  14073  subrg1  14108  subrgdvds  14112  isrrg  14140  rrgeq0i  14141  rrgeq0  14142  domneq0  14149  islmod  14168  islmodd  14170  lmodprop2d  14225  lss1d  14260  cnfldui  14466  znval  14513  znidom  14534  znunit  14536  znrrg  14537  mplelbascoe  14569  ntreq0  14719  ispsmet  14910  psmet0  14914  ismet  14931  isxmet  14932  xmeteq0  14946  metn0  14965  xmetres2  14966  xblss2ps  14991  xblss2  14992  xmseq0  15055  comet  15086  bdxmet  15088  cnmet  15117  ivthdec  15231  ivthreinc  15232  elply2  15322  reeff1o  15360  ioocosf1o  15441  logbgcd1irr  15554  logbgcd1irraplemexp  15555  mpodvdsmulf1o  15577  lgsval  15596  lgsdir  15627  lgsne0  15630  lgsprme0  15634  lgsdirnn0  15639  gausslemma2dlem0c  15643  gausslemma2dlem0i  15649  gausslemma2dlem7  15660  gausslemma2d  15661  lgseisenlem2  15663  lgseisenlem3  15664  lgsquadlem1  15669  lgsquadlem2  15670  lgsquad2lem2  15674  lgsquad3  15676  m1lgs  15677  2lgs  15696  2sqlem7  15713  2sqlem8  15715  2sqlem9  15716  edg0iedg0g  15777  upgredg  15848  bj-charfunbi  15946  2omap  16132  pw1map  16134  pwle2  16137  subctctexmid  16139  peano4nninf  16145  nninfalllem1  16147  nninfsellemdc  16149  nninfsellemeq  16153  nninfsellemqall  16154  nninfsellemeqinf  16155  isomninnlem  16171  trilpolemlt1  16182  trirec0  16185  iswomninnlem  16190  iswomni0  16192  ismkvnnlem  16193  dceqnconst  16201  dcapnconst  16202