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