Metamath Proof Explorer


Theorem eqtrdi

Description: An equality transitivity deduction. (Contributed by NM, 21-Jun-1993)

Ref Expression
Hypotheses eqtrdi.1 φ A = B
eqtrdi.2 B = C
Assertion eqtrdi φ A = C

Proof

Step Hyp Ref Expression
1 eqtrdi.1 φ A = B
2 eqtrdi.2 B = C
3 2 a1i φ B = C
4 1 3 eqtrd φ A = C