Metamath Proof Explorer


Theorem nelir

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

Ref Expression
Hypothesis nelir.1 ¬ 𝐴𝐵
Assertion nelir 𝐴𝐵

Proof

Step Hyp Ref Expression
1 nelir.1 ¬ 𝐴𝐵
2 df-nel ( 𝐴𝐵 ↔ ¬ 𝐴𝐵 )
3 1 2 mpbir 𝐴𝐵