Metamath Proof Explorer


Theorem 3eqtr4g

Description: A chained equality inference, useful for converting to definitions. (Contributed by NM, 21-Jun-1993)

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

Proof

Step Hyp Ref Expression
1 3eqtr4g.1 φ A = B
2 3eqtr4g.2 C = A
3 3eqtr4g.3 D = B
4 2 1 syl5eq φ C = B
5 4 3 syl6eqr φ C = D