Metamath Proof Explorer

Theorem neir

Description: Inference associated with df-ne . (Contributed by BJ, 7-Jul-2018)

Ref Expression
Hypothesis neir.1 
|- -. A = B
Assertion neir 
|- A =/= B

Proof

Step Hyp Ref Expression
1 neir.1 
 |-  -. A = B
2 df-ne 
 |-  ( A =/= B <-> -. A = B )
3 1 2 mpbir 
 |-  A =/= B