Theorem eqeq1d 2166

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 2164	. 2 |- ( A = B -> ( A = C <-> B = C ) )
3	1, 2	syl 14	1 |- ( ph -> ( A = C <-> B = C ) )

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1335

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-gen 1429  ax-4 1490  ax-17 1506  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-cleq 2150

This theorem is referenced by:  rspcedeq1vd  2825  sbceq2g  3053  csbhypf  3069  csbiebt  3070  csbiebg  3073  dfss4st  3340  disjssun  3457  sneqrg  3726  preq12b  3734  preq12bg  3737  disji2  3959  iin0r  4131  opthg  4199  opeqsn  4213  unisucg  4375  opthreg  4516  tfisi  4547  dmsnopg  5058  relcoi1  5118  iotaeq  5144  iotabi  5145  fneq1  5259  fnun  5277  fnresdisj  5281  fnimadisj  5291  fnimaeq0  5292  sbcfng  5318  foeq1  5389  foco  5403  fveqeq2d  5477  fvelimab  5525  fvun1  5535  fvmptdv2  5558  fneqeql  5576  dffo3  5615  fvsng  5664  fconstfvm  5686  eufnfv  5698  f1veqaeq  5720  dff13f  5721  f1elima  5724  foeqcnvco  5741  f1eqcocnv  5742  acexmidlemab  5819  ovanraleqv  5849  eloprabga  5909  ovmpodv2  5955  ovi3  5958  ovelimab  5972  caovcang  5983  caovcan  5986  caovimo  6015  grprinvlem  6016  grpridd  6018  suppssfv  6029  suppssov1  6030  caofinvl  6055  op1stg  6099  op2ndg  6100  eqop  6126  reldm  6135  xporderlem  6179  tposfo2  6215  frec0g  6345  freccllem  6350  frecfcllem  6352  frecsuclem  6354  frecsuc  6355  nnm0r  6427  nnmord  6465  nnaordex  6475  nnawordex  6476  ereq1  6488  eqerlem  6512  mapsn  6636  endisj  6770  xpf1o  6790  mapxpen  6794  fidifsnen  6816  supelti  6947  updjudhcoinlf  7025  updjudhcoinrg  7026  updjud  7027  omp1eomlem  7039  difinfsnlem  7044  nnnninfeq  7072  enomnilem  7082  finomni  7084  exmidomni  7086  fodjuomnilemres  7092  fodjuomni  7093  ismkvnex  7099  mkvprop  7102  fodjumkvlemres  7103  enmkvlem  7105  enwomnilem  7113  pm54.43  7126  exmidfodomrlemrALT  7139  cc2lem  7187  addnidpig  7257  ltexpi  7258  dfplpq2  7275  dfmpq2  7276  recexnq  7311  recmulnqg  7312  ltexnqq  7329  halfnqq  7331  enq0tr  7355  nqnq0pi  7359  addnnnq0  7370  addlocpr  7457  ltexprlemru  7533  ltexpri  7534  lteupri  7538  prplnqu  7541  recexpr  7559  addsrpr  7666  mulsrpr  7667  00sr  7690  negexsr  7693  recexgt0sr  7694  srpospr  7704  prsrriota  7709  caucvgsrlemfv  7712  map2psrprg  7726  elrealeu  7750  axrnegex  7800  axprecex  7801  rereceu  7810  recriota  7811  nntopi  7815  axcaucvglemval  7818  axcaucvglemcau  7819  cnegexlem1  8051  cnegex  8054  cnegex2  8055  subval  8068  subadd  8079  subadd2  8080  subsub23  8081  addsubeq4  8091  subcan2  8101  negcon1  8128  subcan  8131  addrsub  8247  ltadd2  8295  ltordlem  8358  recexre  8454  recexap  8528  muleqadd  8543  receuap  8544  divvalap  8548  divmulap  8549  rec11ap  8584  zdiv  9253  uzin  9472  xaddval  9750  xnn0xadd0  9772  xnegdi  9773  xltadd1  9781  icc0r  9831  fznlem  9944  fseq1m1p1  9998  1fv  10042  fzon  10069  fvinim0ffz  10144  ioo0  10163  ico0  10165  ioc0  10166  flqbi  10193  divfl0  10199  modq0  10232  modqmuladdnn0  10271  addmodlteq  10301  frecuzrdgtcl  10315  frecuzrdgfunlem  10322  seq3f1olemstep  10404  seq3f1olemp  10405  seq3id  10411  seq3z  10414  mulreap  10768  rennim  10906  resqrexlemex  10929  rsqrmo  10931  resqrtcl  10933  rersqrtthlem  10934  sqrtsq2  10947  isumss  11292  fsum00  11363  telfsumo  11367  pwm1geoserap1  11409  prodssdc  11490  absefib  11671  efieq1re  11672  divides  11689  dvdsval2  11690  nndivides  11697  dvds0lem  11701  dvds1lem  11702  dvds2lem  11703  negdvdsb  11707  muldvds1  11716  muldvds2  11717  dvdscmulr  11720  dvdsmulcr  11721  dvdstr  11728  dvdsabseq  11743  divconjdvds  11745  odd2np1lem  11767  odd2np1  11768  even2n  11769  oddm1even  11770  2tp1odd  11779  opeo  11792  omeo  11793  m1exp1  11796  divalgb  11820  gcdaddm  11872  gcdabs1  11877  bezout  11899  gcdmultiple  11908  gcdmultiplez  11909  rplpwr  11915  rppwr  11916  alginv  11928  algcvga  11932  algfx  11933  eucalgval2  11934  coprmdvds  11973  qredeq  11977  qredeu  11978  divgcdcoprm0  11982  divgcdcoprmex  11983  cncongr1  11984  rpexp  12032  rpexp12i  12034  cncongrprm  12036  qnumdenbi  12071  phival  12092  phicl2  12093  dfphi2  12099  phiprmpw  12101  phimullem  12104  eulerthlem1  12106  eulerthlemfi  12107  eulerthlemrprm  12108  eulerthlemth  12111  eulerth  12112  fermltl  12113  hashgcdlem  12117  phisum  12119  odzval  12120  odzdvds  12124  reumodprminv  12132  modprm0  12133  nnnn0modprm0  12134  modprmn0modprm0  12135  coprimeprodsq  12136  coprimeprodsq2  12137  pythagtriplem2  12145  pythagtrip  12162  ennnfonelemhf1o  12184  ntreq0  12574  ispsmet  12765  psmet0  12769  ismet  12786  isxmet  12787  xmeteq0  12801  metn0  12820  xmetres2  12821  xblss2ps  12846  xblss2  12847  xmseq0  12910  comet  12941  bdxmet  12943  cnmet  12972  ivthdec  13064  reeff1o  13136  ioocosf1o  13217  logbgcd1irr  13326  logbgcd1irraplemexp  13327  bj-charfunbi  13428  pwle2  13612  subctctexmid  13615  peano4nninf  13620  nninfalllem1  13622  nninfsellemdc  13624  nninfsellemeq  13628  nninfsellemqall  13629  nninfsellemeqinf  13630  isomninnlem  13643  trilpolemlt1  13654  trirec0  13657  iswomninnlem  13662  iswomni0  13664  ismkvnnlem  13665  dceqnconst  13672  dcapnconst  13673