Metamath Proof Explorer


Theorem niabn

Description: Miscellaneous inference relating falsehoods. (Contributed by NM, 31-Mar-1994)

Ref Expression
Hypothesis niabn.1 φ
Assertion niabn ¬ψχψ¬φ

Proof

Step Hyp Ref Expression
1 niabn.1 φ
2 simpr χψψ
3 1 pm2.24i ¬φψ
4 2 3 pm5.21ni ¬ψχψ¬φ