Metamath Proof Explorer


Theorem 3eqtr4a

Description: A chained equality inference, useful for converting to definitions. (Contributed by NM, 2-Feb-2007) (Proof shortened by Andrew Salmon, 25-May-2011)

Ref Expression
Hypotheses 3eqtr4a.1 A = B
3eqtr4a.2 φ C = A
3eqtr4a.3 φ D = B
Assertion 3eqtr4a φ C = D

Proof

Step Hyp Ref Expression
1 3eqtr4a.1 A = B
2 3eqtr4a.2 φ C = A
3 3eqtr4a.3 φ D = B
4 2 1 eqtrdi φ C = B
5 4 3 eqtr4d φ C = D