Metamath Proof Explorer


Theorem syl6eq

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

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

Proof

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