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

Metamath Proof Explorer

Theorem neeqtrri

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

Ref Expression
Hypotheses neeqtrr.1 ⊢ A ≠ B
neeqtrr.2 ⊢ C = B
Assertion neeqtrri ⊢ A ≠ C

Proof

Step Hyp Ref Expression
1 neeqtrr.1 ⊢ A ≠ B
2 neeqtrr.2 ⊢ C = B
3 2 eqcomi ⊢ B = C
4 1 3 neeqtri ⊢ A ≠ C