Theorem eqeq1d 2243

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 2241	. 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 2216

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

This theorem is referenced by:  rspcedeq1vd  2933  sbceq2g  3163  csbhypf  3180  csbiebt  3181  csbiebg  3184  dfss4st  3458  disjssun  3576  sneqrg  3871  preq12b  3879  preq12bg  3882  disji2  4106  invdisjrab  4108  iin0r  4287  opthg  4359  opeqsn  4374  unisucg  4540  opthreg  4683  tfisi  4714  dmsnopg  5239  relcoi1  5299  iotaeq  5326  iotabi  5327  fneq1  5449  fnun  5469  fnresdisj  5473  fnimadisj  5484  fnimaeq0  5485  sbcfng  5511  foeq1  5591  foco  5606  fveqeq2d  5683  fvelimab  5738  fvun1  5748  fvmptdv2  5772  fneqeql  5791  dffo3  5829  fvsng  5885  fconstfvm  5907  eufnfv  5922  f1veqaeq  5948  dff13f  5949  f1elima  5952  foeqcnvco  5969  f1eqcocnv  5970  acexmidlemab  6052  ovanraleqv  6082  eloprabga  6148  ovmpodv2  6195  ovi3  6199  ovelimab  6213  caovcang  6224  caovcan  6227  caovimo  6256  suppssov1  6272  caofinvl  6301  caofid1  6304  caofid2  6305  uchoice  6344  op1stg  6357  op2ndg  6358  eqop  6384  reldm  6393  xporderlem  6440  suppofss1dcl  6477  suppofss2dcl  6478  tposfo2  6511  frec0g  6641  freccllem  6646  frecfcllem  6648  frecsuclem  6650  frecsuc  6651  nnm0r  6725  nnmord  6763  nnaordex  6774  nnawordex  6775  ereq1  6787  eqerlem  6811  mapsnd  6936  mapsn  6938  endisj  7088  pw2f1odclem  7100  xpf1o  7110  mapxpen  7114  fidifsnen  7138  2omap  7282  supelti  7306  updjudhcoinlf  7384  updjudhcoinrg  7385  updjud  7386  omp1eomlem  7398  difinfsnlem  7403  nnnninfeq  7432  enomnilem  7442  finomni  7444  exmidomni  7446  fodjuomnilemres  7452  fodjuomni  7453  ismkvnex  7459  mkvprop  7462  fodjumkvlemres  7463  enmkvlem  7465  enwomnilem  7473  nninfdcinf  7475  nninfwlporlem  7477  nninfwlpoimlemginf  7480  pm54.43  7500  exmidfodomrlemrALT  7519  cc2lem  7596  addnidpig  7667  ltexpi  7668  dfplpq2  7685  dfmpq2  7686  recexnq  7721  recmulnqg  7722  ltexnqq  7739  halfnqq  7741  enq0tr  7765  nqnq0pi  7769  addnnnq0  7780  addlocpr  7867  ltexprlemru  7943  ltexpri  7944  lteupri  7948  prplnqu  7951  recexpr  7969  addsrpr  8076  mulsrpr  8077  00sr  8100  negexsr  8103  recexgt0sr  8104  srpospr  8114  prsrriota  8119  caucvgsrlemfv  8122  map2psrprg  8136  elrealeu  8160  axrnegex  8210  axprecex  8211  rereceu  8220  recriota  8221  nntopi  8225  axcaucvglemval  8228  axcaucvglemcau  8229  cnegexlem1  8464  cnegex  8467  cnegex2  8468  subval  8481  subadd  8492  subadd2  8493  subsub23  8494  addsubeq4  8504  subcan2  8514  negcon1  8541  subcan  8544  addrsub  8660  ltadd2  8710  ltordlem  8773  recexre  8869  recexap  8944  muleqadd  8959  receuap  8960  divvalap  8965  divmulap  8966  rec11ap  9001  rerecapb  9134  zdiv  9684  uzin  9905  xaddval  10197  xnn0xadd0  10219  xnegdi  10220  xltadd1  10228  icc0r  10278  fznlem  10395  fseq1m1p1  10451  1fv  10495  fzon  10523  fvinim0ffz  10609  ioo0  10643  ico0  10645  ioc0  10646  flqbi  10674  divfl0  10680  modq0  10715  modqmuladdnn0  10754  addmodlteq  10784  frecuzrdgtcl  10798  frecuzrdgfunlem  10805  seq3f1olemstep  10900  seq3f1olemp  10901  seq3id  10911  seq3z  10914  qsqeqor  11036  hashfibc  11232  hashtpglem  11243  ccat0  11309  wrdl1s1  11343  ccatws1lenp1bg  11348  pfxsuff1eqwrdeq  11416  swrdccatin2  11446  pfxccatin12lem2  11448  mulreap  11574  rennim  11712  resqrexlemex  11735  rsqrmo  11737  resqrtcl  11739  rersqrtthlem  11740  sqrtsq2  11753  isumss  12102  fsum00  12173  telfsumo  12177  pwm1geoserap1  12219  prodssdc  12300  absefib  12482  efieq1re  12483  divides  12500  dvdsval2  12501  nndivides  12508  dvds0lem  12512  dvds1lem  12513  dvds2lem  12514  negdvdsb  12518  muldvds1  12527  muldvds2  12528  dvdscmulr  12531  dvdsmulcr  12532  dvdstr  12539  dvdsabseq  12558  divconjdvds  12560  odd2np1lem  12583  odd2np1  12584  even2n  12585  oddm1even  12586  2tp1odd  12595  opeo  12608  omeo  12609  m1exp1  12612  divalgb  12636  gcdaddm  12705  gcdabs1  12710  bezout  12732  gcdmultiple  12741  gcdmultiplez  12742  rplpwr  12748  rppwr  12749  nninfctlemfo  12761  alginv  12769  algcvga  12773  algfx  12774  eucalgval2  12775  coprmdvds  12814  qredeq  12818  qredeu  12819  divgcdcoprm0  12823  divgcdcoprmex  12824  cncongr1  12825  rpexp  12875  rpexp12i  12877  cncongrprm  12879  qnumdenbi  12914  phival  12935  phicl2  12936  dfphi2  12942  phiprmpw  12944  phimullem  12947  eulerthlem1  12949  eulerthlemfi  12950  eulerthlemrprm  12951  eulerthlemth  12954  eulerth  12955  fermltl  12956  hashgcdlem  12960  phisum  12963  odzval  12964  odzdvds  12968  reumodprminv  12976  modprm0  12977  nnnn0modprm0  12978  modprmn0modprm0  12979  coprimeprodsq  12980  coprimeprodsq2  12981  pythagtriplem2  12989  pythagtrip  13006  pceulem  13017  pcval  13019  pcqmul  13026  pcqcl  13029  pcabs  13049  pc2dvds  13053  pcaddlem  13062  pcadd  13063  pcmpt  13066  prmpwdvds  13078  pockthi  13081  4sqlem12  13125  ballotfilemi  13187  ballotfilemi1  13189  ballotfilemii  13190  ballotfilemsima  13203  ballotfilemfrcn0  13217  ballotfi  13226  ennnfonelemhf1o  13248  fvprif  13607  mgmidmo  13635  grpidvalg  13636  grpidpropdg  13637  ismgmid  13640  ismgmid2  13643  mgmidsssn0  13647  grpinvalem  13648  grprida  13650  igsumvalx  13652  gsumress  13658  ismnddef  13679  sgrpidmndm  13681  ismndd  13698  mndpropd  13701  mndinvmod  13706  mnd1  13710  ismhm  13716  gsumvallem2  13748  grpinvex  13765  isgrpd2  13776  isgrpd  13778  dfgrp2  13782  grpinveu  13793  grpinvval  13798  grplinv  13805  isgrpinv  13809  grplrinv  13812  grpidinv2  13813  grpidinv  13814  grplmulf1o  13829  grpsubeq0  13841  grpsubadd  13843  dfgrp3mlem  13853  dfgrp3m  13854  grp1  13861  imasgrp2  13863  qusgrp2  13866  mhmmnd  13869  ghmgrp  13871  mulgval  13875  mulgaddcom  13899  eqg0el  13982  ghmeqker  14024  ghmf1  14026  conjnmzb  14033  ablsubadd  14065  ablsubsub23  14078  gfsumz  14109  rngmneg1  14186  rngmneg2  14187  rng1zrlem  14198  dfur2g  14205  srgideu  14215  srgidmlem  14221  issrgid  14224  srgrz  14227  srglz  14228  srgisid  14229  ringideu  14260  ringidmlem  14265  isringid  14268  ringid  14269  qusring2  14309  oppr0g  14325  oppr1g  14326  dvdsrvald  14338  dvdsrmuld  14341  dvdsr01  14349  dvdsr02  14350  opprunitd  14355  crngunit  14356  unitinvinv  14369  dvreq1  14387  dvdsrpropdg  14392  rhmdvdsr  14420  lringuplu  14441  subrg1  14477  subrgdvds  14481  isrrg  14509  rrgeq0i  14510  rrgeq0  14511  domneq0  14519  islmod  14565  islmodd  14567  lmodprop2d  14622  lss1d  14657  cnfldui  14863  znval  14910  znidom  14931  znunit  14933  znrrg  14934  mplelbascoe  14973  ntreq0  15123  ispsmet  15314  psmet0  15318  ismet  15335  isxmet  15336  xmeteq0  15350  metn0  15369  xmetres2  15370  xblss2ps  15395  xblss2  15396  xmseq0  15459  comet  15490  bdxmet  15492  cnmet  15521  ivthdec  15635  ivthreinc  15636  elply2  15726  reeff1o  15764  ioocosf1o  15845  logbgcd1irr  15958  logbgcd1irraplemexp  15959  mpodvdsmulf1o  15984  lgsval  16003  lgsdir  16034  lgsne0  16037  lgsprme0  16041  lgsdirnn0  16046  gausslemma2dlem0c  16050  gausslemma2dlem0i  16056  gausslemma2dlem7  16067  gausslemma2d  16068  lgseisenlem2  16070  lgseisenlem3  16071  lgsquadlem1  16076  lgsquadlem2  16077  lgsquad2lem2  16081  lgsquad3  16083  m1lgs  16084  2lgs  16103  2sqlem7  16120  2sqlem8  16122  2sqlem9  16123  edg0iedg0g  16187  upgredg  16265  ushgredgedgloop  16349  edg0usgr  16368  vtxdgfval  16409  vtxdgop  16413  vtxdeqd  16417  vtxdfifiun  16418  vtxd0nedgbfi  16420  1loopgrvd2fi  16426  wksfval  16443  wlklenvclwlk  16494  clwwlknon  16550  isclwwlknon  16551  s2elclwwlknon2  16557  depind  16630  bj-charfunbi  16707  pw1map  16895  pwle2  16898  subctctexmid  16900  peano4nninf  16910  nninfalllem1  16912  nninfsellemdc  16914  nninfsellemeq  16918  nninfsellemqall  16919  nninfsellemeqinf  16920  isomninnlem  16940  trilpolemlt1  16951  trirec0  16954  qdiff  16959  iswomninnlem  16960  iswomni0  16962  ismkvnnlem  16963  dceqnconst  16972  dcapnconst  16973