Theorem 3eqtr4d 2131

Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

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

Assertion

Ref	Expression
3eqtr4d	|- ( ph -> C = D )

Proof of Theorem 3eqtr4d

Step	Hyp	Ref	Expression
1		3eqtr4d.2	. 2 |- ( ph -> C = A )
2		3eqtr4d.3	. . 3 |- ( ph -> D = B )
3		3eqtr4d.1	. . 3 |- ( ph -> A = B )
4	2, 3	eqtr4d 2124	. 2 |- ( ph -> D = A )
5	1, 4	eqtr4d 2124	1 |- ( ph -> C = D )

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:  fnsnfv  5378  fvco2  5388  resfunexg  5534  fcof1  5578  fliftfun  5591  caovdir2d  5837  caov32d  5841  caov31d  5843  caov4d  5845  caovlem2d  5853  caofcom  5894  cnvf1olem  6005  tfrlem1  6089  tfrlemisucaccv  6106  tfr1onlemsucaccv  6122  tfrcllemsucaccv  6135  frecrdg  6189  oav2  6240  omv2  6242  omsuc  6249  nnmsucr  6265  ecovicom  6416  ecoviass  6418  ecovidi  6420  carden2bex  6880  addcompig  6951  addasspig  6952  mulcompig  6953  mulasspig  6954  distrpig  6955  addassnqg  7004  addnq0mo  7069  mulnq0mo  7070  nqnq0a  7076  nqnq0m  7077  distrnq0  7081  mulcomnq0  7082  addassnq0  7084  addcmpblnr  7348  mulcmpblnrlemg  7349  addsrmo  7352  mulsrmo  7353  ltsrprg  7356  recexgt0sr  7382  mulgt0sr  7386  mulextsr1lem  7388  addcnsrec  7442  mulcnsrec  7443  pitonnlem2  7447  recidpirqlemcalc  7457  axaddcom  7468  adddir  7542  mul32  7675  mul31  7676  add32  7704  add4  7706  sub32  7779  sub4  7790  subdir  7927  mulneg2  7937  mulreim  8144  apadd1  8148  apneg  8151  divassap  8220  divdirap  8227  divmul13ap  8245  divmul24ap  8246  divdiv32ap  8250  conjmulap  8259  zeo  8914  lincmb01cmp  9483  iccf1o  9484  flhalf  9772  modqvalp1  9813  modqdi  9862  modqsubdir  9863  frecuzrdgg  9886  iseqshft2  9961  iseqcaopr3  9973  iseqcaopr  9975  seq3f1olemqsumkj  9990  seq3f1olemqsumk  9991  seq3f1olemqsum  9992  iseqhomo  10005  seq3homo  10007  iseqdistr  10008  seq3distr  10009  expp1  10025  expnegap0  10026  expaddzaplem  10061  expaddzap  10062  expmulzap  10064  sqneg  10077  sqdivap  10082  subsq2  10125  binom2  10128  facp1  10201  bcm1k  10231  bcp1n  10232  ibcval5  10234  omgadd  10273  hashun  10276  hashxp  10297  shftfibg  10317  shftfib  10320  shftval  10322  2shfti  10328  seq3shft  10335  crre  10354  remim  10357  mulreap  10361  reneg  10365  readd  10366  remullem  10368  redivap  10371  imneg  10373  imadd  10374  imdivap  10378  cjcj  10380  cjadd  10381  cjmulrcl  10384  cjneg  10387  imval2  10391  resqrexlemcalc1  10510  absneg  10546  sqabsadd  10551  sqabssub  10552  absmul  10565  absresq  10574  absexp  10575  absexpzap  10576  serf0  10804  isummolem3  10833  fisum  10841  isumss  10846  fisumss  10847  fsumadd  10863  isummulc1  10884  isumdivapc  10885  fsum2dlemstep  10891  fisumcom2  10895  fisum0diag2  10904  fsummulc2  10905  fsummulc1  10906  fsumdivapc  10907  fsumconst  10911  telfsumo  10923  fsumparts  10927  binomlem  10940  isumshft  10947  arisum2  10956  geolim  10968  geo2sum  10971  geo2lim  10973  cvgratnnlemseq  10983  cvgratz  10989  mertenslem2  10993  efcllemp  11011  efcj  11026  efexp  11035  resinval  11069  recosval  11070  cosneg  11081  efival  11086  sinadd  11090  cosadd  11091  addcos  11100  sin2t  11103  cos2t  11104  odd2np1lem  11213  oexpneg  11218  neggcd  11315  gcdabs2  11322  mulgcd  11346  mulgcdr  11348  gcddiv  11349  rplpwr  11357  eucalgval  11377  eucalginv  11379  eucalg  11382  neglcm  11398  lcmgcd  11401  mulgcddvds  11417  qredeu  11420  nn0gcdsq  11519  phimullem  11542  setsabsd  11596  setscom  11597  tgdom  11835  nninfalllemn  12201  nninfsellemeqinf  12211