Theorem 3eqtr4d 2079

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

Syntax hints:   -> wi 4   = wceq 1242

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-4 1397  ax-17 1416  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-cleq 2030

This theorem is referenced by:  fnsnfv  5175  fvco2  5185  resfunexg  5325  fcof1  5366  fliftfun  5379  caovdir2d  5619  caov32d  5623  caov31d  5625  caov4d  5627  caovlem2d  5635  caofcom  5676  cnvf1olem  5787  tfrlem1  5864  tfrlemisucaccv  5880  frecrdg  5931  oav2  5982  omv2  5984  omsuc  5990  nnmsucr  6006  ecovicom  6150  ecoviass  6152  ecovidi  6154  addcompig  6313  addasspig  6314  mulcompig  6315  mulasspig  6316  distrpig  6317  addassnqg  6366  addnq0mo  6430  mulnq0mo  6431  nqnq0a  6437  nqnq0m  6438  distrnq0  6442  mulcomnq0  6443  addassnq0  6445  addcmpblnr  6667  mulcmpblnrlemg  6668  addsrmo  6671  mulsrmo  6672  ltsrprg  6675  recexgt0sr  6701  mulgt0sr  6704  mulextsr1lem  6706  addcnsrec  6739  mulcnsrec  6740  pitonnlem2  6743  axaddcom  6754  adddir  6816  mul32  6940  mul31  6941  add32  6967  add4  6969  sub32  7041  sub4  7052  subdir  7179  mulneg2  7189  mulreim  7388  apadd1  7392  apneg  7395  divassap  7451  divdirap  7456  divmul13ap  7473  divmul24ap  7474  divdiv32ap  7478  conjmulap  7487  zeo  8119  lincmb01cmp  8641  iccf1o  8642  expp1  8916  expnegap0  8917  expaddzaplem  8952  expaddzap  8953  expmulzap  8955  sqneg  8967  sqdivap  8972  subsq2  9012  binom2  9015  crre  9085  remim  9088  mulreap  9092  reneg  9096  readd  9097  remullem  9099  redivap  9102  imneg  9104  imadd  9105  imdivap  9109  cjcj  9111  cjadd  9112  cjmulrcl  9115  cjneg  9118  imval2  9122  absneg  9219