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

Metamath Proof Explorer

Theorem eqnetri

Description: Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012)

Ref Expression
Hypotheses eqnetr.1 ⊢ A = B
eqnetr.2 ⊢ B ≠ C
Assertion eqnetri ⊢ A ≠ C

Proof

Step Hyp Ref Expression
1 eqnetr.1 ⊢ A = B
2 eqnetr.2 ⊢ B ≠ C
3 1 neeq1i ⊢ A ≠ C ↔ B ≠ C
4 2 3 mpbir ⊢ A ≠ C