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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   = wceq 1402

This proof depends on 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 proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  rspcedeq1vd  2939  sbceq2g  3169  csbhypf  3186  csbiebt  3187  csbiebg  3190  dfss4st  3464  disjssun  3588  sneqrg  3887  preq12b  3895  preq12bg  3898  disji2  4122  invdisjrab  4124  iin0r  4306  opthg  4378  opeqsn  4393  unisucg  4559  opthreg  4703  tfisi  4734  dmsnopg  5259  relcoi1  5319  iotaeq  5346  iotabi  5347  fneq1  5469  fnun  5489  fnresdisj  5493  fnimadisj  5504  fnimaeq0  5505  sbcfng  5531  foeq1  5611  foco  5626  fveqeq2d  5703  fvelimab  5759  fvun1  5769  fvmptdv2  5795  fneqeql  5817  dffo3  5855  fvsng  5911  fconstfvm  5933  eufnfv  5949  f1veqaeq  5975  dff13f  5976  f1elima  5979  foeqcnvco  5996  f1eqcocnv  5997  acexmidlemab  6079  ovanraleqv  6109  eloprabga  6175  ovmpodv2  6222  ovi3  6226  ovelimab  6240  caovcang  6251  caovcan  6254  caovimo  6283  suppssov1  6299  caofinvl  6328  caofid1  6331  caofid2  6332  uchoice  6371  op1stg  6384  op2ndg  6385  eqop  6411  reldm  6420  xporderlem  6467  suppofss1dcl  6504  suppofss2dcl  6505  tposfo2  6538  frec0g  6668  freccllem  6673  frecfcllem  6675  frecsuclem  6677  frecsuc  6678  nnm0r  6752  nnmord  6790  nnaordex  6801  nnawordex  6802  ereq1  6814  eqerlem  6838  mapsnd  6970  mapsn  6972  endisj  7122  pw2f1odclem  7134  xpf1o  7144  mapxpen  7148  fidifsnen  7172  2omap  7318  supelti  7342  updjudhcoinlf  7420  updjudhcoinrg  7421  updjud  7422  omp1eomlem  7434  difinfsnlem  7439  nnnninfeq  7468  enomnilem  7478  finomni  7480  exmidomni  7482  fodjuomnilemres  7488  fodjuomni  7489  ismkvnex  7495  mkvprop  7498  fodjumkvlemres  7499  enmkvlem  7501  enwomnilem  7509  nninfdcinf  7511  nninfwlporlem  7513  nninfwlpoimlemginf  7516  pm54.43  7536  exmidfodomrlemrALT  7555  cc2lem  7632  addnidpig  7703  ltexpi  7704  dfplpq2  7721  dfmpq2  7722  recexnq  7757  recmulnqg  7758  ltexnqq  7775  halfnqq  7777  enq0tr  7801  nqnq0pi  7805  addnnnq0  7816  addlocpr  7903  ltexprlemru  7979  ltexpri  7980  lteupri  7984  prplnqu  7987  recexpr  8005  addsrpr  8112  mulsrpr  8113  00sr  8136  negexsr  8139  recexgt0sr  8140  srpospr  8150  prsrriota  8155  caucvgsrlemfv  8158  map2psrprg  8172  elrealeu  8196  axrnegex  8246  axprecex  8247  rereceu  8256  recriota  8257  nntopi  8261  axcaucvglemval  8264  axcaucvglemcau  8265  cnegexlem1  8502  cnegex  8505  cnegex2  8506  subval  8519  subadd  8530  subadd2  8531  subsub23  8532  addsubeq4  8542  subcan2  8552  negcon1  8579  subcan  8582  addrsub  8698  ltadd2  8748  ltordlem  8811  recexre  8908  recexap  8983  muleqadd  9000  receuap  9001  divvalap  9006  divmulap  9007  rec11ap  9042  rerecapb  9175  zdiv  9738  uzin  9964  xaddval  10257  xnn0xadd0  10279  xnegdi  10280  xltadd1  10288  icc0r  10338  fznlem  10455  fseq1m1p1  10512  1fv  10556  fzon  10584  fvinim0ffz  10670  ioo0  10704  ico0  10706  ioc0  10707  flqbi  10738  divfl0  10744  modq0  10779  modqmuladdnn0  10818  addmodlteq  10848  frecuzrdgtcl  10862  frecuzrdgfunlem  10869  seq3f1olemstep  10964  seq3f1olemp  10965  seq3id  10975  seq3z  10978  qsqeqor  11100  hashfibc  11297  hashf1lem1  11299  hashtpglem  11312  ccat0  11378  wrdl1s1  11412  ccatws1lenp1bg  11417  pfxsuff1eqwrdeq  11485  swrdccatin2  11515  pfxccatin12lem2  11517  mulreap  11643  rennim  11782  resqrexlemex  11805  rsqrmo  11807  resqrtcl  11809  rersqrtthlem  11810  sqrtsq2  11823  isumss  12174  fsum00  12245  telfsumo  12249  pwm1geoserap1  12291  prodssdc  12372  absefib  12554  efieq1re  12555  divides  12572  dvdsval2  12573  nndivides  12580  dvds0lem  12584  dvds1lem  12585  dvds2lem  12586  negdvdsb  12590  muldvds1  12599  muldvds2  12600  dvdscmulr  12603  dvdsmulcr  12604  dvdstr  12611  dvdsabseq  12630  divconjdvds  12632  odd2np1lem  12655  odd2np1  12656  even2n  12657  oddm1even  12658  2tp1odd  12667  opeo  12680  omeo  12681  m1exp1  12684  divalgb  12708  gcdaddm  12777  gcdabs1  12782  bezout  12804  gcdmultiple  12813  gcdmultiplez  12814  rplpwr  12820  rppwr  12821  nninfctlemfo  12833  alginv  12841  algcvga  12845  algfx  12846  eucalgval2  12847  coprmdvds  12886  qredeq  12890  qredeu  12891  divgcdcoprm0  12895  divgcdcoprmex  12896  cncongr1  12897  rpexp  12948  rpexp12i  12950  cncongrprm  12952  qnumdenbi  12988  phival  13011  phicl2  13012  dfphi2  13018  phiprmpw  13020  phimullem  13023  eulerthlem1  13025  eulerthlemfi  13026  eulerthlemrprm  13027  eulerthlemth  13030  eulerth  13031  fermltl  13032  hashgcdlem  13036  phisum  13039  odzval  13040  odzdvds  13044  reumodprminv  13052  modprm0  13053  nnnn0modprm0  13054  modprmn0modprm0  13055  coprimeprodsq  13056  coprimeprodsq2  13057  pythagtriplem2  13065  pythagtrip  13082  pceulem  13093  pcval  13095  pcqmul  13102  pcqcl  13105  pcabs  13125  pc2dvds  13129  pcaddlem  13138  pcadd  13139  pcmpt  13142  prmpwdvds  13154  pockthi  13157  4sqlem12  13201  ballotfilemi  13292  ballotfilemi1  13294  ballotfilemii  13295  ballotfilemsima  13308  ballotfilemfrcn0  13322  ballotfi  13331  ennnfonelemhf1o  13353  fvprif  13713  mgmidmo  13741  grpidvalg  13742  grpidpropdg  13743  ismgmid  13746  ismgmid2  13749  mgmidsssn0  13753  grpinvalem  13754  grprida  13756  gzsumvalx  13758  gzsumress  13761  ismnddef  13780  sgrpidmndm  13782  ismndd  13799  mndpropd  13802  mndinvmod  13807  mnd1  13811  ismhm  13817  gsumvallem2  13849  grpinvex  13864  isgrpd2  13875  isgrpd  13877  dfgrp2  13881  grpinveu  13892  grpinvval  13897  grplinv  13904  isgrpinv  13908  grplrinv  13911  grpidinv2  13912  grpidinv  13913  grplmulf1o  13928  grpsubeq0  13940  grpsubadd  13942  dfgrp3mlem  13952  dfgrp3m  13953  grp1  13960  imasgrp2  13962  qusgrp2  13965  mhmmnd  13968  ghmgrp  13970  mulgval  13974  mulgaddcom  13998  eqg0el  14081  ghmeqker  14123  ghmf1  14125  conjnmzb  14132  ablsubadd  14165  ablsubsub23  14178  gsumzfi  14207  rngmneg1  14295  rngmneg2  14296  rng1zrlem  14307  dfur2g  14315  srgideu  14325  srgidmlem  14331  issrgid  14334  srgrz  14337  srglz  14338  srgisid  14339  ringideu  14370  ringidmlem  14376  isringid  14379  ringid  14380  qusring2  14420  oppr0g  14436  oppr1g  14437  dvdsrvald  14449  dvdsrmuld  14452  dvdsr01  14460  dvdsr02  14461  opprunitd  14466  crngunit  14467  unitinvinv  14480  dvreq1  14498  dvdsrpropdg  14503  rhmdvdsr  14531  lringuplu  14552  subrg1  14588  subrgdvds  14592  isrrg  14620  rrgeq0i  14621  rrgeq0  14622  domneq0  14630  islmod  14676  islmodd  14678  lmodprop2d  14734  lss1d  14769  cnfldui  14973  znval  15020  znidom  15041  znunit  15043  znrrg  15044  mplelbascoe  15132  ntreq0  15282  ispsmet  15473  psmet0  15477  ismet  15494  isxmet  15495  xmeteq0  15509  metn0  15528  xmetres2  15529  xblss2ps  15554  xblss2  15555  xmseq0  15618  comet  15649  bdxmet  15651  cnmet  15680  ivthdec  15794  ivthreinc  15795  elply2  15885  reeff1o  15923  ioocosf1o  16005  logbgcd1irr  16122  logbgcd1irraplemexp  16123  birthdaylem1g  16144  mpodvdsmulf1o  16185  ppiqub  16194  lgsval  16221  lgsdir  16252  lgsne0  16255  lgsprme0  16259  lgsdirnn0  16264  gausslemma2dlem0c  16268  gausslemma2dlem0i  16274  gausslemma2dlem7  16285  gausslemma2d  16286  lgseisenlem2  16288  lgseisenlem3  16289  lgsquadlem1  16294  lgsquadlem2  16295  lgsquad2lem2  16299  lgsquad3  16301  m1lgs  16302  2lgs  16321  2sqlem7  16338  2sqlem8  16340  2sqlem9  16341  edg0iedg0g  16405  upgredg  16483  ushgredgedgloop  16567  edg0usgr  16586  vtxdgfval  16627  vtxdgop  16631  vtxdeqd  16635  vtxdfifiun  16636  vtxd0nedgbfi  16638  1loopgrvd2fi  16644  wksfval  16661  wlklenvclwlk  16712  clwwlknon  16768  isclwwlknon  16769  s2elclwwlknon2  16775  depind  16848  dichmul0orlem7  16857  bj-charfunbi  16935  pw1map  17123  pwle2  17126  subctctexmid  17128  wexmiddifxylem  17143  peano4nninf  17147  nninfalllem1  17149  nninfsellemdc  17151  nninfsellemeq  17155  nninfsellemqall  17156  nninfsellemeqinf  17157  isomninnlem  17177  trilpolemlt1  17188  trirec0  17191  qdiff  17196  iswomninnlem  17197  iswomni0  17199  ismkvnnlem  17200  dceqnconst  17208  dcapnconst  17209