Theorem eqeq1d 2238

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 2236	. 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 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  rspcedeq1vd  2916  sbceq2g  3146  csbhypf  3163  csbiebt  3164  csbiebg  3167  dfss4st  3437  disjssun  3555  sneqrg  3840  preq12b  3848  preq12bg  3851  disji2  4075  invdisjrab  4077  iin0r  4253  opthg  4324  opeqsn  4339  unisucg  4505  opthreg  4648  tfisi  4679  dmsnopg  5200  relcoi1  5260  iotaeq  5287  iotabi  5288  fneq1  5409  fnun  5429  fnresdisj  5433  fnimadisj  5444  fnimaeq0  5445  sbcfng  5471  foeq1  5544  foco  5559  fveqeq2d  5635  fvelimab  5690  fvun1  5700  fvmptdv2  5724  fneqeql  5743  dffo3  5782  fvsng  5835  fconstfvm  5857  eufnfv  5870  f1veqaeq  5893  dff13f  5894  f1elima  5897  foeqcnvco  5914  f1eqcocnv  5915  acexmidlemab  5995  ovanraleqv  6025  eloprabga  6091  ovmpodv2  6138  ovi3  6142  ovelimab  6156  caovcang  6167  caovcan  6170  caovimo  6199  suppssfv  6214  suppssov1  6215  caofinvl  6244  caofid1  6247  caofid2  6248  uchoice  6283  op1stg  6296  op2ndg  6297  eqop  6323  reldm  6332  xporderlem  6377  tposfo2  6413  frec0g  6543  freccllem  6548  frecfcllem  6550  frecsuclem  6552  frecsuc  6553  nnm0r  6625  nnmord  6663  nnaordex  6674  nnawordex  6675  ereq1  6687  eqerlem  6711  mapsn  6837  endisj  6983  pw2f1odclem  6995  xpf1o  7005  mapxpen  7009  fidifsnen  7032  supelti  7169  updjudhcoinlf  7247  updjudhcoinrg  7248  updjud  7249  omp1eomlem  7261  difinfsnlem  7266  nnnninfeq  7295  enomnilem  7305  finomni  7307  exmidomni  7309  fodjuomnilemres  7315  fodjuomni  7316  ismkvnex  7322  mkvprop  7325  fodjumkvlemres  7326  enmkvlem  7328  enwomnilem  7336  nninfdcinf  7338  nninfwlporlem  7340  nninfwlpoimlemginf  7343  pm54.43  7363  exmidfodomrlemrALT  7381  cc2lem  7452  addnidpig  7523  ltexpi  7524  dfplpq2  7541  dfmpq2  7542  recexnq  7577  recmulnqg  7578  ltexnqq  7595  halfnqq  7597  enq0tr  7621  nqnq0pi  7625  addnnnq0  7636  addlocpr  7723  ltexprlemru  7799  ltexpri  7800  lteupri  7804  prplnqu  7807  recexpr  7825  addsrpr  7932  mulsrpr  7933  00sr  7956  negexsr  7959  recexgt0sr  7960  srpospr  7970  prsrriota  7975  caucvgsrlemfv  7978  map2psrprg  7992  elrealeu  8016  axrnegex  8066  axprecex  8067  rereceu  8076  recriota  8077  nntopi  8081  axcaucvglemval  8084  axcaucvglemcau  8085  cnegexlem1  8321  cnegex  8324  cnegex2  8325  subval  8338  subadd  8349  subadd2  8350  subsub23  8351  addsubeq4  8361  subcan2  8371  negcon1  8398  subcan  8401  addrsub  8517  ltadd2  8566  ltordlem  8629  recexre  8725  recexap  8800  muleqadd  8815  receuap  8816  divvalap  8821  divmulap  8822  rec11ap  8857  rerecapb  8990  zdiv  9535  uzin  9755  xaddval  10041  xnn0xadd0  10063  xnegdi  10064  xltadd1  10072  icc0r  10122  fznlem  10237  fseq1m1p1  10291  1fv  10335  fzon  10363  fvinim0ffz  10447  ioo0  10479  ico0  10481  ioc0  10482  flqbi  10510  divfl0  10516  modq0  10551  modqmuladdnn0  10590  addmodlteq  10620  frecuzrdgtcl  10634  frecuzrdgfunlem  10641  seq3f1olemstep  10736  seq3f1olemp  10737  seq3id  10747  seq3z  10750  qsqeqor  10872  ccat0  11131  wrdl1s1  11163  ccatws1lenp1bg  11168  pfxsuff1eqwrdeq  11231  swrdccatin2  11261  pfxccatin12lem2  11263  mulreap  11375  rennim  11513  resqrexlemex  11536  rsqrmo  11538  resqrtcl  11540  rersqrtthlem  11541  sqrtsq2  11554  isumss  11902  fsum00  11973  telfsumo  11977  pwm1geoserap1  12019  prodssdc  12100  absefib  12282  efieq1re  12283  divides  12300  dvdsval2  12301  nndivides  12308  dvds0lem  12312  dvds1lem  12313  dvds2lem  12314  negdvdsb  12318  muldvds1  12327  muldvds2  12328  dvdscmulr  12331  dvdsmulcr  12332  dvdstr  12339  dvdsabseq  12358  divconjdvds  12360  odd2np1lem  12383  odd2np1  12384  even2n  12385  oddm1even  12386  2tp1odd  12395  opeo  12408  omeo  12409  m1exp1  12412  divalgb  12436  gcdaddm  12505  gcdabs1  12510  bezout  12532  gcdmultiple  12541  gcdmultiplez  12542  rplpwr  12548  rppwr  12549  nninfctlemfo  12561  alginv  12569  algcvga  12573  algfx  12574  eucalgval2  12575  coprmdvds  12614  qredeq  12618  qredeu  12619  divgcdcoprm0  12623  divgcdcoprmex  12624  cncongr1  12625  rpexp  12675  rpexp12i  12677  cncongrprm  12679  qnumdenbi  12714  phival  12735  phicl2  12736  dfphi2  12742  phiprmpw  12744  phimullem  12747  eulerthlem1  12749  eulerthlemfi  12750  eulerthlemrprm  12751  eulerthlemth  12754  eulerth  12755  fermltl  12756  hashgcdlem  12760  phisum  12763  odzval  12764  odzdvds  12768  reumodprminv  12776  modprm0  12777  nnnn0modprm0  12778  modprmn0modprm0  12779  coprimeprodsq  12780  coprimeprodsq2  12781  pythagtriplem2  12789  pythagtrip  12806  pceulem  12817  pcval  12819  pcqmul  12826  pcqcl  12829  pcabs  12849  pc2dvds  12853  pcaddlem  12862  pcadd  12863  pcmpt  12866  prmpwdvds  12878  pockthi  12881  4sqlem12  12925  ennnfonelemhf1o  12984  fvprif  13376  mgmidmo  13405  grpidvalg  13406  grpidpropdg  13407  ismgmid  13410  ismgmid2  13413  mgmidsssn0  13417  grpinvalem  13418  grprida  13420  igsumvalx  13422  gsumress  13428  ismnddef  13451  sgrpidmndm  13453  ismndd  13470  mndpropd  13473  mndinvmod  13478  mnd1  13488  ismhm  13494  gsumvallem2  13526  grpinvex  13543  isgrpd2  13554  isgrpd  13556  dfgrp2  13560  grpinveu  13571  grpinvval  13576  grplinv  13583  isgrpinv  13587  grplrinv  13590  grpidinv2  13591  grpidinv  13592  grplmulf1o  13607  grpsubeq0  13619  grpsubadd  13621  dfgrp3mlem  13631  dfgrp3m  13632  grp1  13639  imasgrp2  13647  qusgrp2  13650  mhmmnd  13653  ghmgrp  13655  mulgval  13659  mulgaddcom  13683  eqg0el  13766  ghmeqker  13808  ghmf1  13810  conjnmzb  13817  ablsubadd  13849  ablsubsub23  13862  rngmneg1  13910  rngmneg2  13911  dfur2g  13925  srgideu  13935  srgidmlem  13941  issrgid  13944  srgrz  13947  srglz  13948  srgisid  13949  srg1zr  13950  ringideu  13980  ringidmlem  13985  isringid  13988  ringid  13989  qusring2  14029  oppr0g  14044  oppr1g  14045  dvdsrvald  14057  dvdsrmuld  14060  dvdsr01  14068  dvdsr02  14069  opprunitd  14074  crngunit  14075  unitinvinv  14088  dvreq1  14106  dvdsrpropdg  14111  rhmdvdsr  14139  lringuplu  14160  subrg1  14195  subrgdvds  14199  isrrg  14227  rrgeq0i  14228  rrgeq0  14229  domneq0  14236  islmod  14255  islmodd  14257  lmodprop2d  14312  lss1d  14347  cnfldui  14553  znval  14600  znidom  14621  znunit  14623  znrrg  14624  mplelbascoe  14656  ntreq0  14806  ispsmet  14997  psmet0  15001  ismet  15018  isxmet  15019  xmeteq0  15033  metn0  15052  xmetres2  15053  xblss2ps  15078  xblss2  15079  xmseq0  15142  comet  15173  bdxmet  15175  cnmet  15204  ivthdec  15318  ivthreinc  15319  elply2  15409  reeff1o  15447  ioocosf1o  15528  logbgcd1irr  15641  logbgcd1irraplemexp  15642  mpodvdsmulf1o  15664  lgsval  15683  lgsdir  15714  lgsne0  15717  lgsprme0  15721  lgsdirnn0  15726  gausslemma2dlem0c  15730  gausslemma2dlem0i  15736  gausslemma2dlem7  15747  gausslemma2d  15748  lgseisenlem2  15750  lgseisenlem3  15751  lgsquadlem1  15756  lgsquadlem2  15757  lgsquad2lem2  15761  lgsquad3  15763  m1lgs  15764  2lgs  15783  2sqlem7  15800  2sqlem8  15802  2sqlem9  15803  edg0iedg0g  15866  upgredg  15942  ushgredgedgloop  16026  wksfval  16035  wlklenvclwlk  16084  bj-charfunbi  16174  2omap  16359  pw1map  16361  pwle2  16364  subctctexmid  16366  peano4nninf  16372  nninfalllem1  16374  nninfsellemdc  16376  nninfsellemeq  16380  nninfsellemqall  16381  nninfsellemeqinf  16382  isomninnlem  16398  trilpolemlt1  16409  trirec0  16412  iswomninnlem  16417  iswomni0  16419  ismkvnnlem  16420  dceqnconst  16428  dcapnconst  16429