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