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 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  rspcedeq1vd  2919  sbceq2g  3149  csbhypf  3166  csbiebt  3167  csbiebg  3170  dfss4st  3440  disjssun  3558  sneqrg  3845  preq12b  3853  preq12bg  3856  disji2  4080  invdisjrab  4082  iin0r  4259  opthg  4330  opeqsn  4345  unisucg  4511  opthreg  4654  tfisi  4685  dmsnopg  5208  relcoi1  5268  iotaeq  5295  iotabi  5296  fneq1  5418  fnun  5438  fnresdisj  5442  fnimadisj  5453  fnimaeq0  5454  sbcfng  5480  foeq1  5555  foco  5570  fveqeq2d  5647  fvelimab  5702  fvun1  5712  fvmptdv2  5736  fneqeql  5755  dffo3  5794  fvsng  5850  fconstfvm  5872  eufnfv  5885  f1veqaeq  5910  dff13f  5911  f1elima  5914  foeqcnvco  5931  f1eqcocnv  5932  acexmidlemab  6012  ovanraleqv  6042  eloprabga  6108  ovmpodv2  6155  ovi3  6159  ovelimab  6173  caovcang  6184  caovcan  6187  caovimo  6216  suppssfv  6231  suppssov1  6232  caofinvl  6261  caofid1  6264  caofid2  6265  uchoice  6300  op1stg  6313  op2ndg  6314  eqop  6340  reldm  6349  xporderlem  6396  tposfo2  6433  frec0g  6563  freccllem  6568  frecfcllem  6570  frecsuclem  6572  frecsuc  6573  nnm0r  6647  nnmord  6685  nnaordex  6696  nnawordex  6697  ereq1  6709  eqerlem  6733  mapsn  6859  endisj  7008  pw2f1odclem  7020  xpf1o  7030  mapxpen  7034  fidifsnen  7057  supelti  7201  updjudhcoinlf  7279  updjudhcoinrg  7280  updjud  7281  omp1eomlem  7293  difinfsnlem  7298  nnnninfeq  7327  enomnilem  7337  finomni  7339  exmidomni  7341  fodjuomnilemres  7347  fodjuomni  7348  ismkvnex  7354  mkvprop  7357  fodjumkvlemres  7358  enmkvlem  7360  enwomnilem  7368  nninfdcinf  7370  nninfwlporlem  7372  nninfwlpoimlemginf  7375  pm54.43  7395  exmidfodomrlemrALT  7414  cc2lem  7485  addnidpig  7556  ltexpi  7557  dfplpq2  7574  dfmpq2  7575  recexnq  7610  recmulnqg  7611  ltexnqq  7628  halfnqq  7630  enq0tr  7654  nqnq0pi  7658  addnnnq0  7669  addlocpr  7756  ltexprlemru  7832  ltexpri  7833  lteupri  7837  prplnqu  7840  recexpr  7858  addsrpr  7965  mulsrpr  7966  00sr  7989  negexsr  7992  recexgt0sr  7993  srpospr  8003  prsrriota  8008  caucvgsrlemfv  8011  map2psrprg  8025  elrealeu  8049  axrnegex  8099  axprecex  8100  rereceu  8109  recriota  8110  nntopi  8114  axcaucvglemval  8117  axcaucvglemcau  8118  cnegexlem1  8354  cnegex  8357  cnegex2  8358  subval  8371  subadd  8382  subadd2  8383  subsub23  8384  addsubeq4  8394  subcan2  8404  negcon1  8431  subcan  8434  addrsub  8550  ltadd2  8599  ltordlem  8662  recexre  8758  recexap  8833  muleqadd  8848  receuap  8849  divvalap  8854  divmulap  8855  rec11ap  8890  rerecapb  9023  zdiv  9568  uzin  9789  xaddval  10080  xnn0xadd0  10102  xnegdi  10103  xltadd1  10111  icc0r  10161  fznlem  10276  fseq1m1p1  10330  1fv  10374  fzon  10402  fvinim0ffz  10488  ioo0  10520  ico0  10522  ioc0  10523  flqbi  10551  divfl0  10557  modq0  10592  modqmuladdnn0  10631  addmodlteq  10661  frecuzrdgtcl  10675  frecuzrdgfunlem  10682  seq3f1olemstep  10777  seq3f1olemp  10778  seq3id  10788  seq3z  10791  qsqeqor  10913  hashtpglem  11111  ccat0  11177  wrdl1s1  11211  ccatws1lenp1bg  11216  pfxsuff1eqwrdeq  11284  swrdccatin2  11314  pfxccatin12lem2  11316  mulreap  11442  rennim  11580  resqrexlemex  11603  rsqrmo  11605  resqrtcl  11607  rersqrtthlem  11608  sqrtsq2  11621  isumss  11970  fsum00  12041  telfsumo  12045  pwm1geoserap1  12087  prodssdc  12168  absefib  12350  efieq1re  12351  divides  12368  dvdsval2  12369  nndivides  12376  dvds0lem  12380  dvds1lem  12381  dvds2lem  12382  negdvdsb  12386  muldvds1  12395  muldvds2  12396  dvdscmulr  12399  dvdsmulcr  12400  dvdstr  12407  dvdsabseq  12426  divconjdvds  12428  odd2np1lem  12451  odd2np1  12452  even2n  12453  oddm1even  12454  2tp1odd  12463  opeo  12476  omeo  12477  m1exp1  12480  divalgb  12504  gcdaddm  12573  gcdabs1  12578  bezout  12600  gcdmultiple  12609  gcdmultiplez  12610  rplpwr  12616  rppwr  12617  nninfctlemfo  12629  alginv  12637  algcvga  12641  algfx  12642  eucalgval2  12643  coprmdvds  12682  qredeq  12686  qredeu  12687  divgcdcoprm0  12691  divgcdcoprmex  12692  cncongr1  12693  rpexp  12743  rpexp12i  12745  cncongrprm  12747  qnumdenbi  12782  phival  12803  phicl2  12804  dfphi2  12810  phiprmpw  12812  phimullem  12815  eulerthlem1  12817  eulerthlemfi  12818  eulerthlemrprm  12819  eulerthlemth  12822  eulerth  12823  fermltl  12824  hashgcdlem  12828  phisum  12831  odzval  12832  odzdvds  12836  reumodprminv  12844  modprm0  12845  nnnn0modprm0  12846  modprmn0modprm0  12847  coprimeprodsq  12848  coprimeprodsq2  12849  pythagtriplem2  12857  pythagtrip  12874  pceulem  12885  pcval  12887  pcqmul  12894  pcqcl  12897  pcabs  12917  pc2dvds  12921  pcaddlem  12930  pcadd  12931  pcmpt  12934  prmpwdvds  12946  pockthi  12949  4sqlem12  12993  ennnfonelemhf1o  13052  fvprif  13444  mgmidmo  13473  grpidvalg  13474  grpidpropdg  13475  ismgmid  13478  ismgmid2  13481  mgmidsssn0  13485  grpinvalem  13486  grprida  13488  igsumvalx  13490  gsumress  13496  ismnddef  13519  sgrpidmndm  13521  ismndd  13538  mndpropd  13541  mndinvmod  13546  mnd1  13556  ismhm  13562  gsumvallem2  13594  grpinvex  13611  isgrpd2  13622  isgrpd  13624  dfgrp2  13628  grpinveu  13639  grpinvval  13644  grplinv  13651  isgrpinv  13655  grplrinv  13658  grpidinv2  13659  grpidinv  13660  grplmulf1o  13675  grpsubeq0  13687  grpsubadd  13689  dfgrp3mlem  13699  dfgrp3m  13700  grp1  13707  imasgrp2  13715  qusgrp2  13718  mhmmnd  13721  ghmgrp  13723  mulgval  13727  mulgaddcom  13751  eqg0el  13834  ghmeqker  13876  ghmf1  13878  conjnmzb  13885  ablsubadd  13917  ablsubsub23  13930  rngmneg1  13979  rngmneg2  13980  dfur2g  13994  srgideu  14004  srgidmlem  14010  issrgid  14013  srgrz  14016  srglz  14017  srgisid  14018  srg1zr  14019  ringideu  14049  ringidmlem  14054  isringid  14057  ringid  14058  qusring2  14098  oppr0g  14113  oppr1g  14114  dvdsrvald  14126  dvdsrmuld  14129  dvdsr01  14137  dvdsr02  14138  opprunitd  14143  crngunit  14144  unitinvinv  14157  dvreq1  14175  dvdsrpropdg  14180  rhmdvdsr  14208  lringuplu  14229  subrg1  14264  subrgdvds  14268  isrrg  14296  rrgeq0i  14297  rrgeq0  14298  domneq0  14305  islmod  14324  islmodd  14326  lmodprop2d  14381  lss1d  14416  cnfldui  14622  znval  14669  znidom  14690  znunit  14692  znrrg  14693  mplelbascoe  14725  ntreq0  14875  ispsmet  15066  psmet0  15070  ismet  15087  isxmet  15088  xmeteq0  15102  metn0  15121  xmetres2  15122  xblss2ps  15147  xblss2  15148  xmseq0  15211  comet  15242  bdxmet  15244  cnmet  15273  ivthdec  15387  ivthreinc  15388  elply2  15478  reeff1o  15516  ioocosf1o  15597  logbgcd1irr  15710  logbgcd1irraplemexp  15711  mpodvdsmulf1o  15733  lgsval  15752  lgsdir  15783  lgsne0  15786  lgsprme0  15790  lgsdirnn0  15795  gausslemma2dlem0c  15799  gausslemma2dlem0i  15805  gausslemma2dlem7  15816  gausslemma2d  15817  lgseisenlem2  15819  lgseisenlem3  15820  lgsquadlem1  15825  lgsquadlem2  15826  lgsquad2lem2  15830  lgsquad3  15832  m1lgs  15833  2lgs  15852  2sqlem7  15869  2sqlem8  15871  2sqlem9  15872  edg0iedg0g  15936  upgredg  16014  ushgredgedgloop  16098  edg0usgr  16117  vtxdgfval  16158  vtxdgop  16162  vtxdeqd  16166  vtxdfifiun  16167  vtxd0nedgbfi  16169  1loopgrvd2fi  16175  wksfval  16192  wlklenvclwlk  16243  clwwlknon  16299  isclwwlknon  16300  s2elclwwlknon2  16306  depind  16379  bj-charfunbi  16457  2omap  16645  pw1map  16647  pwle2  16650  subctctexmid  16652  peano4nninf  16659  nninfalllem1  16661  nninfsellemdc  16663  nninfsellemeq  16667  nninfsellemqall  16668  nninfsellemeqinf  16669  isomninnlem  16685  trilpolemlt1  16696  trirec0  16699  qdiff  16704  iswomninnlem  16705  iswomni0  16707  ismkvnnlem  16708  dceqnconst  16716  dcapnconst  16717