Metamath Proof Explorer

Theorem neii

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

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

Proof

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