Theorem eqtr4d 2124

Description: An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.)

Hypotheses

Ref	Expression
eqtr4d.1	|- ( ph -> A = B )
eqtr4d.2	|- ( ph -> C = B )

Assertion

Ref	Expression
eqtr4d	|- ( ph -> A = C )

Proof of Theorem eqtr4d

Step	Hyp	Ref	Expression
1		eqtr4d.1	. 2 |- ( ph -> A = B )
2		eqtr4d.2	. . 3 |- ( ph -> C = B )
3	2	eqcomd 2094	. 2 |- ( ph -> B = C )
4	1, 3	eqtrd 2121	1 |- ( ph -> A = C )

Syntax hints:   -> wi 4   = wceq 1290

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1382  ax-gen 1384  ax-4 1446  ax-17 1465  ax-ext 2071

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

This theorem is referenced by:  3eqtr2d  2127  3eqtr2rd  2128  3eqtr4d  2131  3eqtr4rd  2132  3eqtr4a  2147  sbnfc2  2991  ifsbdc  3411  ifeq1dadc  3427  eqifdc  3431  ifandc  3433  onsucuni2  4395  relop  4601  riinint  4709  iotauni  5007  fniinfv  5377  fsn2  5487  fmptapd  5504  fconst2g  5528  fniunfv  5557  ofres  5885  ofco  5889  frecsuclem  6187  frecrdg  6189  oasuc  6241  nnacom  6261  nnaass  6262  nndi  6263  nnmass  6264  nnmsucr  6265  nnmcom  6266  funresdfunsndc  6281  uniqs2  6368  en1bg  6573  fundmen  6579  1domsn  6591  mapxpen  6620  xpmapenlem  6621  phplem4dom  6634  en2eqpr  6679  sbthlemi5  6726  djur  6813  ctmlemr  6846  infnninf  6868  addcmpblnq  6989  distrnqg  7009  ltexnqq  7030  addcmpblnq0  7065  nqnq0a  7076  nqnq0m  7077  nq0m0r  7078  nq0a0  7079  nnanq0  7080  distrnq0  7081  prarloclemlo  7116  prarloclemcalc  7124  genpassl  7146  genpassu  7147  ltsosr  7373  0idsr  7376  1idsr  7377  mulextsr1lem  7388  cnegex  7723  subsub3  7777  subadd4  7789  mulneg12  7938  mulsub  7942  apreap  8127  cru  8142  recextlem1  8183  cju  8484  halfaddsub  8713  nn0supp  8788  nneo  8912  zeo2  8915  uzin  9114  iccf1o  9484  fzsuc2  9556  flqeqceilz  9788  zmod1congr  9811  modqcyc  9829  modqcyc2  9830  modqaddabs  9832  modqmul1  9847  modqaddmulmod  9861  addmodlteq  9868  frec2uzrdg  9879  frecuzrdgsuctlem  9893  iseqvalt  9936  seq3val  9937  iseqoveq  9948  iseqsst  9949  iseqfveq2  9953  seq3fveq2  9955  seq3split  9970  iseqsplit  9971  iseqdistr  10008  seq3distr  10009  iser0f  10011  ser0f  10013  expp1  10025  mulexp  10057  mulexpzap  10058  expadd  10060  expaddzap  10062  expmul  10063  expmulzap  10064  expsubap  10066  expdivap  10069  subsq  10124  mulbinom2  10133  binom3  10134  bernneq  10137  nn0opthd  10193  faclbnd  10212  faclbnd6  10215  bccmpl  10225  bcp1n  10232  zfz1isolemiso  10307  iseqcoll  10310  shftval2  10323  shftval4  10325  seq3shft  10335  crre  10354  remim  10357  remullem  10368  cjexp  10390  cnrecnv  10407  resqrexlemlo  10509  resqrexlemcalc1  10510  resqrexlemcalc2  10511  resqrexlemcalc3  10512  resqrexlemnm  10514  rsqrmo  10523  abscj  10548  absid  10567  absre  10573  recvalap  10593  maxabsle  10700  maxltsup  10714  2zsupmax  10720  climaddc1  10780  climmulc2  10782  climsubc1  10783  climsubc2  10784  climcvg1nlem  10801  isummolem3  10833  zisum  10837  iisum  10838  isumz  10844  isumss  10846  fisumss  10847  fisumcvg2  10849  fsum3cvg2  10850  fsumadd  10863  isummulc2  10883  sumsplitdc  10889  fsum2dlemstep  10891  fisumcom2  10895  fisum0diag2  10904  fsumconst  10911  telfsumo  10923  fsumparts  10927  fsumrelem  10928  binomlem  10940  isumshft  10947  isumsplit  10948  arisum  10955  arisum2  10956  trireciplem  10957  geolim2  10969  geo2sum  10971  0.999...  10978  cvgratz  10989  mertensabs  10994  ef0lem  11013  efval2  11018  ege2le3  11024  efaddlem  11027  efsub  11034  eftlub  11043  efsep  11044  tanval3ap  11068  efi4p  11071  sinneg  11080  sinmul  11098  sincossq  11102  cos2t  11104  demoivreALT  11126  eirraplem  11127  odd2np1  11214  omoe  11237  divalglemex  11263  divalglemeuneg  11264  divalgmod  11268  flodddiv4  11275  gcdneg  11314  gcdaddm  11316  modgcd  11323  bezoutlemnewy  11326  gcdass  11345  gcdmultiple  11350  algrp1  11369  lcmneg  11397  lcmgcdeq  11406  lcmass  11408  cncongr2  11427  prmexpb  11471  sqrt2irr  11482  2sqpwodd  11495  qnumdenbi  11511  phiprmpw  11539  strslfv3  11602  0nninf  12196  nninfalllemn  12201