Theorem 3eqtr4d 2123

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 2116	. 2 |- ( ph -> D = A )
5	1, 4	eqtr4d 2116	1 |- ( ph -> C = D )

Syntax hints:   -> wi 4   = wceq 1284

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-4 1440  ax-17 1459  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-cleq 2074

This theorem is referenced by:  fnsnfv  5253  fvco2  5263  resfunexg  5403  fcof1  5443  fliftfun  5456  caovdir2d  5697  caov32d  5701  caov31d  5703  caov4d  5705  caovlem2d  5713  caofcom  5754  cnvf1olem  5865  tfrlem1  5946  tfrlemisucaccv  5962  frecrdg  6015  oav2  6066  omv2  6068  omsuc  6074  nnmsucr  6090  ecovicom  6237  ecoviass  6239  ecovidi  6241  carden2bex  6458  addcompig  6519  addasspig  6520  mulcompig  6521  mulasspig  6522  distrpig  6523  addassnqg  6572  addnq0mo  6637  mulnq0mo  6638  nqnq0a  6644  nqnq0m  6645  distrnq0  6649  mulcomnq0  6650  addassnq0  6652  addcmpblnr  6916  mulcmpblnrlemg  6917  addsrmo  6920  mulsrmo  6921  ltsrprg  6924  recexgt0sr  6950  mulgt0sr  6954  mulextsr1lem  6956  addcnsrec  7010  mulcnsrec  7011  pitonnlem2  7015  recidpirqlemcalc  7025  axaddcom  7036  adddir  7110  mul32  7238  mul31  7239  add32  7267  add4  7269  sub32  7342  sub4  7353  subdir  7490  mulneg2  7500  mulreim  7704  apadd1  7708  apneg  7711  divassap  7778  divdirap  7785  divmul13ap  7803  divmul24ap  7804  divdiv32ap  7808  conjmulap  7817  zeo  8452  lincmb01cmp  9025  iccf1o  9026  flhalf  9304  modqvalp1  9345  modqdi  9394  modqsubdir  9395  iseqshft2  9452  iseqcaopr3  9460  iseqcaopr  9462  iseqhomo  9468  iseqdistr  9470  expp1  9483  expnegap0  9484  expaddzaplem  9519  expaddzap  9520  expmulzap  9522  sqneg  9535  sqdivap  9540  subsq2  9582  binom2  9585  facp1  9657  bcm1k  9687  bcp1n  9688  ibcval5  9690  shftfibg  9708  shftfib  9711  shftval  9713  2shfti  9719  crre  9744  remim  9747  mulreap  9751  reneg  9755  readd  9756  remullem  9758  redivap  9761  imneg  9763  imadd  9764  imdivap  9768  cjcj  9770  cjadd  9771  cjmulrcl  9774  cjneg  9777  imval2  9781  resqrexlemcalc1  9900  absneg  9936  sqabsadd  9941  sqabssub  9942  absmul  9955  absresq  9964  absexp  9965  absexpzap  9966  serif0  10189  odd2np1lem  10271  oexpneg  10276  neggcd  10374  gcdabs2  10381  mulgcd  10405  mulgcdr  10407  gcddiv  10408  rplpwr  10416  eucalgval  10436  eucalginv  10438  eucialg  10441  neglcm  10457  lcmgcd  10460  mulgcddvds  10476  qredeu  10479