Theorem eqeq1d 2240

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 2238	. 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 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

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

This theorem is referenced by:  rspcedeq1vd  2920  sbceq2g  3150  csbhypf  3167  csbiebt  3168  csbiebg  3171  dfss4st  3442  disjssun  3560  sneqrg  3850  preq12b  3858  preq12bg  3861  disji2  4085  invdisjrab  4087  iin0r  4265  opthg  4336  opeqsn  4351  unisucg  4517  opthreg  4660  tfisi  4691  dmsnopg  5215  relcoi1  5275  iotaeq  5302  iotabi  5303  fneq1  5425  fnun  5445  fnresdisj  5449  fnimadisj  5460  fnimaeq0  5461  sbcfng  5487  foeq1  5564  foco  5579  fveqeq2d  5656  fvelimab  5711  fvun1  5721  fvmptdv2  5745  fneqeql  5764  dffo3  5802  fvsng  5858  fconstfvm  5880  eufnfv  5895  f1veqaeq  5920  dff13f  5921  f1elima  5924  foeqcnvco  5941  f1eqcocnv  5942  acexmidlemab  6022  ovanraleqv  6052  eloprabga  6118  ovmpodv2  6165  ovi3  6169  ovelimab  6183  caovcang  6194  caovcan  6197  caovimo  6226  suppssov1  6241  caofinvl  6270  caofid1  6273  caofid2  6274  uchoice  6309  op1stg  6322  op2ndg  6323  eqop  6349  reldm  6358  xporderlem  6405  suppofss1dcl  6442  suppofss2dcl  6443  tposfo2  6476  frec0g  6606  freccllem  6611  frecfcllem  6613  frecsuclem  6615  frecsuc  6616  nnm0r  6690  nnmord  6728  nnaordex  6739  nnawordex  6740  ereq1  6752  eqerlem  6776  mapsn  6902  endisj  7051  pw2f1odclem  7063  xpf1o  7073  mapxpen  7077  fidifsnen  7100  supelti  7261  updjudhcoinlf  7339  updjudhcoinrg  7340  updjud  7341  omp1eomlem  7353  difinfsnlem  7358  nnnninfeq  7387  enomnilem  7397  finomni  7399  exmidomni  7401  fodjuomnilemres  7407  fodjuomni  7408  ismkvnex  7414  mkvprop  7417  fodjumkvlemres  7418  enmkvlem  7420  enwomnilem  7428  nninfdcinf  7430  nninfwlporlem  7432  nninfwlpoimlemginf  7435  pm54.43  7455  exmidfodomrlemrALT  7474  cc2lem  7545  addnidpig  7616  ltexpi  7617  dfplpq2  7634  dfmpq2  7635  recexnq  7670  recmulnqg  7671  ltexnqq  7688  halfnqq  7690  enq0tr  7714  nqnq0pi  7718  addnnnq0  7729  addlocpr  7816  ltexprlemru  7892  ltexpri  7893  lteupri  7897  prplnqu  7900  recexpr  7918  addsrpr  8025  mulsrpr  8026  00sr  8049  negexsr  8052  recexgt0sr  8053  srpospr  8063  prsrriota  8068  caucvgsrlemfv  8071  map2psrprg  8085  elrealeu  8109  axrnegex  8159  axprecex  8160  rereceu  8169  recriota  8170  nntopi  8174  axcaucvglemval  8177  axcaucvglemcau  8178  cnegexlem1  8413  cnegex  8416  cnegex2  8417  subval  8430  subadd  8441  subadd2  8442  subsub23  8443  addsubeq4  8453  subcan2  8463  negcon1  8490  subcan  8493  addrsub  8609  ltadd2  8658  ltordlem  8721  recexre  8817  recexap  8892  muleqadd  8907  receuap  8908  divvalap  8913  divmulap  8914  rec11ap  8949  rerecapb  9082  zdiv  9629  uzin  9850  xaddval  10141  xnn0xadd0  10163  xnegdi  10164  xltadd1  10172  icc0r  10222  fznlem  10338  fseq1m1p1  10392  1fv  10436  fzon  10464  fvinim0ffz  10550  ioo0  10582  ico0  10584  ioc0  10585  flqbi  10613  divfl0  10619  modq0  10654  modqmuladdnn0  10693  addmodlteq  10723  frecuzrdgtcl  10737  frecuzrdgfunlem  10744  seq3f1olemstep  10839  seq3f1olemp  10840  seq3id  10850  seq3z  10853  qsqeqor  10975  hashtpglem  11173  ccat0  11239  wrdl1s1  11273  ccatws1lenp1bg  11278  pfxsuff1eqwrdeq  11346  swrdccatin2  11376  pfxccatin12lem2  11378  mulreap  11504  rennim  11642  resqrexlemex  11665  rsqrmo  11667  resqrtcl  11669  rersqrtthlem  11670  sqrtsq2  11683  isumss  12032  fsum00  12103  telfsumo  12107  pwm1geoserap1  12149  prodssdc  12230  absefib  12412  efieq1re  12413  divides  12430  dvdsval2  12431  nndivides  12438  dvds0lem  12442  dvds1lem  12443  dvds2lem  12444  negdvdsb  12448  muldvds1  12457  muldvds2  12458  dvdscmulr  12461  dvdsmulcr  12462  dvdstr  12469  dvdsabseq  12488  divconjdvds  12490  odd2np1lem  12513  odd2np1  12514  even2n  12515  oddm1even  12516  2tp1odd  12525  opeo  12538  omeo  12539  m1exp1  12542  divalgb  12566  gcdaddm  12635  gcdabs1  12640  bezout  12662  gcdmultiple  12671  gcdmultiplez  12672  rplpwr  12678  rppwr  12679  nninfctlemfo  12691  alginv  12699  algcvga  12703  algfx  12704  eucalgval2  12705  coprmdvds  12744  qredeq  12748  qredeu  12749  divgcdcoprm0  12753  divgcdcoprmex  12754  cncongr1  12755  rpexp  12805  rpexp12i  12807  cncongrprm  12809  qnumdenbi  12844  phival  12865  phicl2  12866  dfphi2  12872  phiprmpw  12874  phimullem  12877  eulerthlem1  12879  eulerthlemfi  12880  eulerthlemrprm  12881  eulerthlemth  12884  eulerth  12885  fermltl  12886  hashgcdlem  12890  phisum  12893  odzval  12894  odzdvds  12898  reumodprminv  12906  modprm0  12907  nnnn0modprm0  12908  modprmn0modprm0  12909  coprimeprodsq  12910  coprimeprodsq2  12911  pythagtriplem2  12919  pythagtrip  12936  pceulem  12947  pcval  12949  pcqmul  12956  pcqcl  12959  pcabs  12979  pc2dvds  12983  pcaddlem  12992  pcadd  12993  pcmpt  12996  prmpwdvds  13008  pockthi  13011  4sqlem12  13055  ennnfonelemhf1o  13114  fvprif  13506  mgmidmo  13535  grpidvalg  13536  grpidpropdg  13537  ismgmid  13540  ismgmid2  13543  mgmidsssn0  13547  grpinvalem  13548  grprida  13550  igsumvalx  13552  gsumress  13558  ismnddef  13581  sgrpidmndm  13583  ismndd  13600  mndpropd  13603  mndinvmod  13608  mnd1  13618  ismhm  13624  gsumvallem2  13656  grpinvex  13673  isgrpd2  13684  isgrpd  13686  dfgrp2  13690  grpinveu  13701  grpinvval  13706  grplinv  13713  isgrpinv  13717  grplrinv  13720  grpidinv2  13721  grpidinv  13722  grplmulf1o  13737  grpsubeq0  13749  grpsubadd  13751  dfgrp3mlem  13761  dfgrp3m  13762  grp1  13769  imasgrp2  13777  qusgrp2  13780  mhmmnd  13783  ghmgrp  13785  mulgval  13789  mulgaddcom  13813  eqg0el  13896  ghmeqker  13938  ghmf1  13940  conjnmzb  13947  ablsubadd  13979  ablsubsub23  13992  rngmneg1  14041  rngmneg2  14042  dfur2g  14056  srgideu  14066  srgidmlem  14072  issrgid  14075  srgrz  14078  srglz  14079  srgisid  14080  srg1zr  14081  ringideu  14111  ringidmlem  14116  isringid  14119  ringid  14120  qusring2  14160  oppr0g  14175  oppr1g  14176  dvdsrvald  14188  dvdsrmuld  14191  dvdsr01  14199  dvdsr02  14200  opprunitd  14205  crngunit  14206  unitinvinv  14219  dvreq1  14237  dvdsrpropdg  14242  rhmdvdsr  14270  lringuplu  14291  subrg1  14326  subrgdvds  14330  isrrg  14358  rrgeq0i  14359  rrgeq0  14360  domneq0  14368  islmod  14387  islmodd  14389  lmodprop2d  14444  lss1d  14479  cnfldui  14685  znval  14732  znidom  14753  znunit  14755  znrrg  14756  mplelbascoe  14793  ntreq0  14943  ispsmet  15134  psmet0  15138  ismet  15155  isxmet  15156  xmeteq0  15170  metn0  15189  xmetres2  15190  xblss2ps  15215  xblss2  15216  xmseq0  15279  comet  15310  bdxmet  15312  cnmet  15341  ivthdec  15455  ivthreinc  15456  elply2  15546  reeff1o  15584  ioocosf1o  15665  logbgcd1irr  15778  logbgcd1irraplemexp  15779  mpodvdsmulf1o  15804  lgsval  15823  lgsdir  15854  lgsne0  15857  lgsprme0  15861  lgsdirnn0  15866  gausslemma2dlem0c  15870  gausslemma2dlem0i  15876  gausslemma2dlem7  15887  gausslemma2d  15888  lgseisenlem2  15890  lgseisenlem3  15891  lgsquadlem1  15896  lgsquadlem2  15897  lgsquad2lem2  15901  lgsquad3  15903  m1lgs  15904  2lgs  15923  2sqlem7  15940  2sqlem8  15942  2sqlem9  15943  edg0iedg0g  16007  upgredg  16085  ushgredgedgloop  16169  edg0usgr  16188  vtxdgfval  16229  vtxdgop  16233  vtxdeqd  16237  vtxdfifiun  16238  vtxd0nedgbfi  16240  1loopgrvd2fi  16246  wksfval  16263  wlklenvclwlk  16314  clwwlknon  16370  isclwwlknon  16371  s2elclwwlknon2  16377  depind  16450  bj-charfunbi  16527  2omap  16715  pw1map  16717  pwle2  16720  subctctexmid  16722  peano4nninf  16732  nninfalllem1  16734  nninfsellemdc  16736  nninfsellemeq  16740  nninfsellemqall  16741  nninfsellemeqinf  16742  isomninnlem  16762  trilpolemlt1  16773  trirec0  16776  qdiff  16781  iswomninnlem  16782  iswomni0  16784  ismkvnnlem  16785  dceqnconst  16793  dcapnconst  16794