Theorem eqeq1d 2247

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 2245	. 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 1402

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  rspcedeq1vd  2939  sbceq2g  3169  csbhypf  3186  csbiebt  3187  csbiebg  3190  dfss4st  3464  disjssun  3587  sneqrg  3882  preq12b  3890  preq12bg  3893  disji2  4117  invdisjrab  4119  iin0r  4301  opthg  4373  opeqsn  4388  unisucg  4554  opthreg  4698  tfisi  4729  dmsnopg  5254  relcoi1  5314  iotaeq  5341  iotabi  5342  fneq1  5464  fnun  5484  fnresdisj  5488  fnimadisj  5499  fnimaeq0  5500  sbcfng  5526  foeq1  5606  foco  5621  fveqeq2d  5698  fvelimab  5753  fvun1  5763  fvmptdv2  5789  fneqeql  5808  dffo3  5846  fvsng  5902  fconstfvm  5924  eufnfv  5939  f1veqaeq  5965  dff13f  5966  f1elima  5969  foeqcnvco  5986  f1eqcocnv  5987  acexmidlemab  6069  ovanraleqv  6099  eloprabga  6165  ovmpodv2  6212  ovi3  6216  ovelimab  6230  caovcang  6241  caovcan  6244  caovimo  6273  suppssov1  6289  caofinvl  6318  caofid1  6321  caofid2  6322  uchoice  6361  op1stg  6374  op2ndg  6375  eqop  6401  reldm  6410  xporderlem  6457  suppofss1dcl  6494  suppofss2dcl  6495  tposfo2  6528  frec0g  6658  freccllem  6663  frecfcllem  6665  frecsuclem  6667  frecsuc  6668  nnm0r  6742  nnmord  6780  nnaordex  6791  nnawordex  6792  ereq1  6804  eqerlem  6828  mapsnd  6960  mapsn  6962  endisj  7112  pw2f1odclem  7124  xpf1o  7134  mapxpen  7138  fidifsnen  7162  2omap  7308  supelti  7332  updjudhcoinlf  7410  updjudhcoinrg  7411  updjud  7412  omp1eomlem  7424  difinfsnlem  7429  nnnninfeq  7458  enomnilem  7468  finomni  7470  exmidomni  7472  fodjuomnilemres  7478  fodjuomni  7479  ismkvnex  7485  mkvprop  7488  fodjumkvlemres  7489  enmkvlem  7491  enwomnilem  7499  nninfdcinf  7501  nninfwlporlem  7503  nninfwlpoimlemginf  7506  pm54.43  7526  exmidfodomrlemrALT  7545  cc2lem  7622  addnidpig  7693  ltexpi  7694  dfplpq2  7711  dfmpq2  7712  recexnq  7747  recmulnqg  7748  ltexnqq  7765  halfnqq  7767  enq0tr  7791  nqnq0pi  7795  addnnnq0  7806  addlocpr  7893  ltexprlemru  7969  ltexpri  7970  lteupri  7974  prplnqu  7977  recexpr  7995  addsrpr  8102  mulsrpr  8103  00sr  8126  negexsr  8129  recexgt0sr  8130  srpospr  8140  prsrriota  8145  caucvgsrlemfv  8148  map2psrprg  8162  elrealeu  8186  axrnegex  8236  axprecex  8237  rereceu  8246  recriota  8247  nntopi  8251  axcaucvglemval  8254  axcaucvglemcau  8255  cnegexlem1  8491  cnegex  8494  cnegex2  8495  subval  8508  subadd  8519  subadd2  8520  subsub23  8521  addsubeq4  8531  subcan2  8541  negcon1  8568  subcan  8571  addrsub  8687  ltadd2  8737  ltordlem  8800  recexre  8896  recexap  8971  muleqadd  8988  receuap  8989  divvalap  8994  divmulap  8995  rec11ap  9030  rerecapb  9163  zdiv  9713  uzin  9934  xaddval  10226  xnn0xadd0  10248  xnegdi  10249  xltadd1  10257  icc0r  10307  fznlem  10424  fseq1m1p1  10480  1fv  10524  fzon  10552  fvinim0ffz  10638  ioo0  10672  ico0  10674  ioc0  10675  flqbi  10703  divfl0  10709  modq0  10744  modqmuladdnn0  10783  addmodlteq  10813  frecuzrdgtcl  10827  frecuzrdgfunlem  10834  seq3f1olemstep  10929  seq3f1olemp  10930  seq3id  10940  seq3z  10943  qsqeqor  11065  hashfibc  11261  hashf1lem1  11263  hashtpglem  11276  ccat0  11342  wrdl1s1  11376  ccatws1lenp1bg  11381  pfxsuff1eqwrdeq  11449  swrdccatin2  11479  pfxccatin12lem2  11481  mulreap  11607  rennim  11746  resqrexlemex  11769  rsqrmo  11771  resqrtcl  11773  rersqrtthlem  11774  sqrtsq2  11787  isumss  12136  fsum00  12207  telfsumo  12211  pwm1geoserap1  12253  prodssdc  12334  absefib  12516  efieq1re  12517  divides  12534  dvdsval2  12535  nndivides  12542  dvds0lem  12546  dvds1lem  12547  dvds2lem  12548  negdvdsb  12552  muldvds1  12561  muldvds2  12562  dvdscmulr  12565  dvdsmulcr  12566  dvdstr  12573  dvdsabseq  12592  divconjdvds  12594  odd2np1lem  12617  odd2np1  12618  even2n  12619  oddm1even  12620  2tp1odd  12629  opeo  12642  omeo  12643  m1exp1  12646  divalgb  12670  gcdaddm  12739  gcdabs1  12744  bezout  12766  gcdmultiple  12775  gcdmultiplez  12776  rplpwr  12782  rppwr  12783  nninfctlemfo  12795  alginv  12803  algcvga  12807  algfx  12808  eucalgval2  12809  coprmdvds  12848  qredeq  12852  qredeu  12853  divgcdcoprm0  12857  divgcdcoprmex  12858  cncongr1  12859  rpexp  12909  rpexp12i  12911  cncongrprm  12913  qnumdenbi  12948  phival  12969  phicl2  12970  dfphi2  12976  phiprmpw  12978  phimullem  12981  eulerthlem1  12983  eulerthlemfi  12984  eulerthlemrprm  12985  eulerthlemth  12988  eulerth  12989  fermltl  12990  hashgcdlem  12994  phisum  12997  odzval  12998  odzdvds  13002  reumodprminv  13010  modprm0  13011  nnnn0modprm0  13012  modprmn0modprm0  13013  coprimeprodsq  13014  coprimeprodsq2  13015  pythagtriplem2  13023  pythagtrip  13040  pceulem  13051  pcval  13053  pcqmul  13060  pcqcl  13063  pcabs  13083  pc2dvds  13087  pcaddlem  13096  pcadd  13097  pcmpt  13100  prmpwdvds  13112  pockthi  13115  4sqlem12  13159  ballotfilemi  13221  ballotfilemi1  13223  ballotfilemii  13224  ballotfilemsima  13237  ballotfilemfrcn0  13251  ballotfi  13260  ennnfonelemhf1o  13282  fvprif  13641  mgmidmo  13669  grpidvalg  13670  grpidpropdg  13671  ismgmid  13674  ismgmid2  13677  mgmidsssn0  13681  grpinvalem  13682  grprida  13684  gzsumvalx  13686  gzsumress  13689  ismnddef  13708  sgrpidmndm  13710  ismndd  13727  mndpropd  13730  mndinvmod  13735  mnd1  13739  ismhm  13745  gsumvallem2  13777  grpinvex  13792  isgrpd2  13803  isgrpd  13805  dfgrp2  13809  grpinveu  13820  grpinvval  13825  grplinv  13832  isgrpinv  13836  grplrinv  13839  grpidinv2  13840  grpidinv  13841  grplmulf1o  13856  grpsubeq0  13868  grpsubadd  13870  dfgrp3mlem  13880  dfgrp3m  13881  grp1  13888  imasgrp2  13890  qusgrp2  13893  mhmmnd  13896  ghmgrp  13898  mulgval  13902  mulgaddcom  13926  eqg0el  14009  ghmeqker  14051  ghmf1  14053  conjnmzb  14060  ablsubadd  14093  ablsubsub23  14106  gsumzfi  14135  rngmneg1  14221  rngmneg2  14222  rng1zrlem  14233  dfur2g  14240  srgideu  14250  srgidmlem  14256  issrgid  14259  srgrz  14262  srglz  14263  srgisid  14264  ringideu  14295  ringidmlem  14300  isringid  14303  ringid  14304  qusring2  14344  oppr0g  14360  oppr1g  14361  dvdsrvald  14373  dvdsrmuld  14376  dvdsr01  14384  dvdsr02  14385  opprunitd  14390  crngunit  14391  unitinvinv  14404  dvreq1  14422  dvdsrpropdg  14427  rhmdvdsr  14455  lringuplu  14476  subrg1  14512  subrgdvds  14516  isrrg  14544  rrgeq0i  14545  rrgeq0  14546  domneq0  14554  islmod  14600  islmodd  14602  lmodprop2d  14657  lss1d  14692  cnfldui  14896  znval  14943  znidom  14964  znunit  14966  znrrg  14967  mplelbascoe  15006  ntreq0  15156  ispsmet  15347  psmet0  15351  ismet  15368  isxmet  15369  xmeteq0  15383  metn0  15402  xmetres2  15403  xblss2ps  15428  xblss2  15429  xmseq0  15492  comet  15523  bdxmet  15525  cnmet  15554  ivthdec  15668  ivthreinc  15669  elply2  15759  reeff1o  15797  ioocosf1o  15878  logbgcd1irr  15992  logbgcd1irraplemexp  15993  mpodvdsmulf1o  16018  lgsval  16037  lgsdir  16068  lgsne0  16071  lgsprme0  16075  lgsdirnn0  16080  gausslemma2dlem0c  16084  gausslemma2dlem0i  16090  gausslemma2dlem7  16101  gausslemma2d  16102  lgseisenlem2  16104  lgseisenlem3  16105  lgsquadlem1  16110  lgsquadlem2  16111  lgsquad2lem2  16115  lgsquad3  16117  m1lgs  16118  2lgs  16137  2sqlem7  16154  2sqlem8  16156  2sqlem9  16157  edg0iedg0g  16221  upgredg  16299  ushgredgedgloop  16383  edg0usgr  16402  vtxdgfval  16443  vtxdgop  16447  vtxdeqd  16451  vtxdfifiun  16452  vtxd0nedgbfi  16454  1loopgrvd2fi  16460  wksfval  16477  wlklenvclwlk  16528  clwwlknon  16584  isclwwlknon  16585  s2elclwwlknon2  16591  depind  16664  dichmul0orlem7  16673  bj-charfunbi  16751  pw1map  16939  pwle2  16942  subctctexmid  16944  peano4nninf  16954  nninfalllem1  16956  nninfsellemdc  16958  nninfsellemeq  16962  nninfsellemqall  16963  nninfsellemeqinf  16964  isomninnlem  16984  trilpolemlt1  16995  trirec0  16998  qdiff  17003  iswomninnlem  17004  iswomni0  17006  ismkvnnlem  17007  dceqnconst  17015  dcapnconst  17016