Metamath Proof Explorer


Theorem 3eqtr2rd

Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006)

Ref Expression
Hypotheses 3eqtr2d.1
|- ( ph -> A = B )
3eqtr2d.2
|- ( ph -> C = B )
3eqtr2d.3
|- ( ph -> C = D )
Assertion 3eqtr2rd
|- ( ph -> D = A )

Proof

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