Metamath Proof Explorer


Theorem eqtrid

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

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

Proof

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