This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eqtr4id

Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998)

Ref Expression
Hypotheses eqtr4id.2 ⊢ A = B
eqtr4id.1 ⊢ φ → C = B
Assertion eqtr4id ⊢ φ → A = C

Proof

Step Hyp Ref Expression
1 eqtr4id.2 ⊢ A = B
2 eqtr4id.1 ⊢ φ → C = B
3 1 eqcomi ⊢ B = A
4 2 3 eqtr2di ⊢ φ → A = C