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  iin0r  4213  opthg  4282  opeqsn  4297  unisucg  4461  opthreg  4604  tfisi  4635  dmsnopg  5154  relcoi1  5214  iotaeq  5240  iotabi  5241  fneq1  5362  fnun  5382  fnresdisj  5386  fnimadisj  5396  fnimaeq0  5397  sbcfng  5423  foeq1  5494  foco  5509  fveqeq2d  5584  fvelimab  5635  fvun1  5645  fvmptdv2  5669  fneqeql  5688  dffo3  5727  fvsng  5780  fconstfvm  5802  eufnfv  5815  f1veqaeq  5838  dff13f  5839  f1elima  5842  foeqcnvco  5859  f1eqcocnv  5860  acexmidlemab  5938  ovanraleqv  5968  eloprabga  6032  ovmpodv2  6079  ovi3  6083  ovelimab  6097  caovcang  6108  caovcan  6111  caovimo  6140  suppssfv  6154  suppssov1  6155  caofinvl  6184  caofid1  6187  caofid2  6188  uchoice  6223  op1stg  6236  op2ndg  6237  eqop  6263  reldm  6272  xporderlem  6317  tposfo2  6353  frec0g  6483  freccllem  6488  frecfcllem  6490  frecsuclem  6492  frecsuc  6493  nnm0r  6565  nnmord  6603  nnaordex  6614  nnawordex  6615  ereq1  6627  eqerlem  6651  mapsn  6777  endisj  6919  pw2f1odclem  6931  xpf1o  6941  mapxpen  6945  fidifsnen  6967  supelti  7104  updjudhcoinlf  7182  updjudhcoinrg  7183  updjud  7184  omp1eomlem  7196  difinfsnlem  7201  nnnninfeq  7230  enomnilem  7240  finomni  7242  exmidomni  7244  fodjuomnilemres  7250  fodjuomni  7251  ismkvnex  7257  mkvprop  7260  fodjumkvlemres  7261  enmkvlem  7263  enwomnilem  7271  nninfdcinf  7273  nninfwlporlem  7275  nninfwlpoimlemginf  7278  pm54.43  7298  exmidfodomrlemrALT  7311  cc2lem  7378  addnidpig  7449  ltexpi  7450  dfplpq2  7467  dfmpq2  7468  recexnq  7503  recmulnqg  7504  ltexnqq  7521  halfnqq  7523  enq0tr  7547  nqnq0pi  7551  addnnnq0  7562  addlocpr  7649  ltexprlemru  7725  ltexpri  7726  lteupri  7730  prplnqu  7733  recexpr  7751  addsrpr  7858  mulsrpr  7859  00sr  7882  negexsr  7885  recexgt0sr  7886  srpospr  7896  prsrriota  7901  caucvgsrlemfv  7904  map2psrprg  7918  elrealeu  7942  axrnegex  7992  axprecex  7993  rereceu  8002  recriota  8003  nntopi  8007  axcaucvglemval  8010  axcaucvglemcau  8011  cnegexlem1  8247  cnegex  8250  cnegex2  8251  subval  8264  subadd  8275  subadd2  8276  subsub23  8277  addsubeq4  8287  subcan2  8297  negcon1  8324  subcan  8327  addrsub  8443  ltadd2  8492  ltordlem  8555  recexre  8651  recexap  8726  muleqadd  8741  receuap  8742  divvalap  8747  divmulap  8748  rec11ap  8783  rerecapb  8916  zdiv  9461  uzin  9681  xaddval  9967  xnn0xadd0  9989  xnegdi  9990  xltadd1  9998  icc0r  10048  fznlem  10163  fseq1m1p1  10217  1fv  10261  fzon  10289  fvinim0ffz  10370  ioo0  10402  ico0  10404  ioc0  10405  flqbi  10433  divfl0  10439  modq0  10474  modqmuladdnn0  10513  addmodlteq  10543  frecuzrdgtcl  10557  frecuzrdgfunlem  10564  seq3f1olemstep  10659  seq3f1olemp  10660  seq3id  10670  seq3z  10673  qsqeqor  10795  ccat0  11052  wrdl1s1  11084  ccatws1lenp1bg  11089  mulreap  11175  rennim  11313  resqrexlemex  11336  rsqrmo  11338  resqrtcl  11340  rersqrtthlem  11341  sqrtsq2  11354  isumss  11702  fsum00  11773  telfsumo  11777  pwm1geoserap1  11819  prodssdc  11900  absefib  12082  efieq1re  12083  divides  12100  dvdsval2  12101  nndivides  12108  dvds0lem  12112  dvds1lem  12113  dvds2lem  12114  negdvdsb  12118  muldvds1  12127  muldvds2  12128  dvdscmulr  12131  dvdsmulcr  12132  dvdstr  12139  dvdsabseq  12158  divconjdvds  12160  odd2np1lem  12183  odd2np1  12184  even2n  12185  oddm1even  12186  2tp1odd  12195  opeo  12208  omeo  12209  m1exp1  12212  divalgb  12236  gcdaddm  12305  gcdabs1  12310  bezout  12332  gcdmultiple  12341  gcdmultiplez  12342  rplpwr  12348  rppwr  12349  nninfctlemfo  12361  alginv  12369  algcvga  12373  algfx  12374  eucalgval2  12375  coprmdvds  12414  qredeq  12418  qredeu  12419  divgcdcoprm0  12423  divgcdcoprmex  12424  cncongr1  12425  rpexp  12475  rpexp12i  12477  cncongrprm  12479  qnumdenbi  12514  phival  12535  phicl2  12536  dfphi2  12542  phiprmpw  12544  phimullem  12547  eulerthlem1  12549  eulerthlemfi  12550  eulerthlemrprm  12551  eulerthlemth  12554  eulerth  12555  fermltl  12556  hashgcdlem  12560  phisum  12563  odzval  12564  odzdvds  12568  reumodprminv  12576  modprm0  12577  nnnn0modprm0  12578  modprmn0modprm0  12579  coprimeprodsq  12580  coprimeprodsq2  12581  pythagtriplem2  12589  pythagtrip  12606  pceulem  12617  pcval  12619  pcqmul  12626  pcqcl  12629  pcabs  12649  pc2dvds  12653  pcaddlem  12662  pcadd  12663  pcmpt  12666  prmpwdvds  12678  pockthi  12681  4sqlem12  12725  ennnfonelemhf1o  12784  fvprif  13175  mgmidmo  13204  grpidvalg  13205  grpidpropdg  13206  ismgmid  13209  ismgmid2  13212  mgmidsssn0  13216  grpinvalem  13217  grprida  13219  igsumvalx  13221  gsumress  13227  ismnddef  13250  sgrpidmndm  13252  ismndd  13269  mndpropd  13272  mndinvmod  13277  mnd1  13287  ismhm  13293  gsumvallem2  13325  grpinvex  13342  isgrpd2  13353  isgrpd  13355  dfgrp2  13359  grpinveu  13370  grpinvval  13375  grplinv  13382  isgrpinv  13386  grplrinv  13389  grpidinv2  13390  grpidinv  13391  grplmulf1o  13406  grpsubeq0  13418  grpsubadd  13420  dfgrp3mlem  13430  dfgrp3m  13431  grp1  13438  imasgrp2  13446  qusgrp2  13449  mhmmnd  13452  ghmgrp  13454  mulgval  13458  mulgaddcom  13482  eqg0el  13565  ghmeqker  13607  ghmf1  13609  conjnmzb  13616  ablsubadd  13648  ablsubsub23  13661  rngmneg1  13709  rngmneg2  13710  dfur2g  13724  srgideu  13734  srgidmlem  13740  issrgid  13743  srgrz  13746  srglz  13747  srgisid  13748  srg1zr  13749  ringideu  13779  ringidmlem  13784  isringid  13787  ringid  13788  qusring2  13828  oppr0g  13843  oppr1g  13844  reldvdsrsrg  13854  dvdsrvald  13855  dvdsrmuld  13858  dvdsr01  13866  dvdsr02  13867  opprunitd  13872  crngunit  13873  unitinvinv  13886  dvreq1  13904  dvdsrpropdg  13909  rhmdvdsr  13937  lringuplu  13958  subrg1  13993  subrgdvds  13997  isrrg  14025  rrgeq0i  14026  rrgeq0  14027  domneq0  14034  islmod  14053  islmodd  14055  lmodprop2d  14110  lss1d  14145  cnfldui  14351  znval  14398  znidom  14419  znunit  14421  znrrg  14422  mplelbascoe  14454  ntreq0  14604  ispsmet  14795  psmet0  14799  ismet  14816  isxmet  14817  xmeteq0  14831  metn0  14850  xmetres2  14851  xblss2ps  14876  xblss2  14877  xmseq0  14940  comet  14971  bdxmet  14973  cnmet  15002  ivthdec  15116  ivthreinc  15117  elply2  15207  reeff1o  15245  ioocosf1o  15326  logbgcd1irr  15439  logbgcd1irraplemexp  15440  mpodvdsmulf1o  15462  lgsval  15481  lgsdir  15512  lgsne0  15515  lgsprme0  15519  lgsdirnn0  15524  gausslemma2dlem0c  15528  gausslemma2dlem0i  15534  gausslemma2dlem7  15545  gausslemma2d  15546  lgseisenlem2  15548  lgseisenlem3  15549  lgsquadlem1  15554  lgsquadlem2  15555  lgsquad2lem2  15559  lgsquad3  15561  m1lgs  15562  2lgs  15581  2sqlem7  15598  2sqlem8  15600  2sqlem9  15601  bj-charfunbi  15747  2omap  15932  pwle2  15935  subctctexmid  15937  peano4nninf  15943  nninfalllem1  15945  nninfsellemdc  15947  nninfsellemeq  15951  nninfsellemqall  15952  nninfsellemeqinf  15953  isomninnlem  15969  trilpolemlt1  15980  trirec0  15983  iswomninnlem  15988  iswomni0  15990  ismkvnnlem  15991  dceqnconst  15999  dcapnconst  16000