Theorem 3eqtrd 1132

Description: A deduction from three chained equalities.

Hypotheses

Ref	Expression
3eqtrd.1	⊢ (φ → A = B)
3eqtrd.2	⊢ (φ → B = C)
3eqtrd.3	⊢ (φ → C = D)

Assertion

Ref	Expression
3eqtrd	⊢ (φ → A = D)

Proof of Theorem 3eqtrd

Step	Hyp	Ref	Expression
1		3eqtrd.1	. 2 ⊢ (φ → A = B)
2		3eqtrd.2	. . 3 ⊢ (φ → B = C)
3		3eqtrd.3	. . 3 ⊢ (φ → C = D)
4	2, 3	eqtrd 1128	. 2 ⊢ (φ → B = D)
5	1, 4	eqtrd 1128	1 ⊢ (φ → A = D)

Syntax hints:   → wi 2   = wceq 1091

This theorem is referenced by:  om1 3144  oe1 3146  ltexpq 3874  halfpq 3876  axcnre 4087  addsubt 4151  negdi2t 4201  subsubt 4203  div23t 4240  divdivdivt 4265  uzind 4603  uzrdgsuc 4659  facp1t 4873  hvsubcan1t 5016  his5 5050  bcs 5101  chocuni 5179  pjthlem7 5231  pjthlem8 5232  5oalem2 5545  5oalem3 5546  5oalem5 5548  3oalem2 5553  pjv 5589  hoid0 5614  pjclem4 5653  pj3s 5659  strlem1 5691  stcltrlem1 5709

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-cleq 1097

metamath.org