Theorem 3eqtr4rd 2181

Description: A deduction from three chained equalities. (Contributed by NM, 21-Sep-1995.)

Hypotheses

Ref	Expression
3eqtr4d.1	⊢ (𝜑 → 𝐴 = 𝐵)
3eqtr4d.2	⊢ (𝜑 → 𝐶 = 𝐴)
3eqtr4d.3	⊢ (𝜑 → 𝐷 = 𝐵)

Assertion

Ref	Expression
3eqtr4rd	⊢ (𝜑 → 𝐷 = 𝐶)

Proof of Theorem 3eqtr4rd

Step	Hyp	Ref	Expression
1		3eqtr4d.3	. . 3 ⊢ (𝜑 → 𝐷 = 𝐵)
2		3eqtr4d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3	1, 2	eqtr4d 2173	. 2 ⊢ (𝜑 → 𝐷 = 𝐴)
4		3eqtr4d.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐴)
5	3, 4	eqtr4d 2173	1 ⊢ (𝜑 → 𝐷 = 𝐶)

Syntax hints:   → wi 4   = wceq 1331

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 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2119

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

This theorem is referenced by:  csbcnvg  4718  fvco4  5486  phplem4  6742  phplem4on  6754  omp1eomlem  6972  ctssdclemn0  6988  recexnq  7191  prarloclemcalc  7303  addcomprg  7379  mulcomprg  7381  mulcmpblnrlemg  7541  axmulass  7674  divnegap  8459  modqlt  10099  modqmulnn  10108  seq3val  10224  seqvalcd  10225  seq3caopr3  10247  seq3f1olemqsumkj  10264  seq3f1olemqsumk  10265  seq3f1olemqsum  10266  seq3f1o  10270  bcval5  10502  omgadd  10541  seq3coll  10578  cjreb  10631  recj  10632  imcj  10640  imval2  10659  resqrexlemover  10775  sqrtmul  10800  amgm2  10883  maxabslemab  10971  xrmaxadd  11023  summodclem2a  11143  fsumf1o  11152  sumsnf  11171  sumsplitdc  11194  fsummulc2  11210  binom  11246  bcxmas  11251  expcnvap0  11264  expcnv  11266  cvgratnnlemnexp  11286  cvgratnnlemmn  11287  ege2le3  11366  efaddlem  11369  eftlub  11385  tanval3ap  11410  tannegap  11424  cosmul  11441  cos01bnd  11454  demoivreALT  11469  flodddiv4  11620  dfgcd3  11687  absmulgcd  11694  sqpweven  11842  2sqpwodd  11843  crth  11889  ctiunctlemfo  11941  setsslnid  11999  txbasval  12425