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

Metamath Proof Explorer

Theorem eqtr3i

Description: An equality transitivity inference. (Contributed by NM, 6-May-1994)

Ref Expression
Hypotheses eqtr3i.1 ⊢ 𝐴 = 𝐵
eqtr3i.2 ⊢ 𝐴 = 𝐶
Assertion eqtr3i 𝐵 = 𝐶

Proof

Step Hyp Ref Expression
1 eqtr3i.1 ⊢ 𝐴 = 𝐵
2 eqtr3i.2 ⊢ 𝐴 = 𝐶
3 1 eqcomi ⊢ 𝐵 = 𝐴
4 3 2 eqtri ⊢ 𝐵 = 𝐶