Theorem niabn

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

Hypothesis
niabn.1
\( \vdash \varphi \)
Conclusion
\( \vdash \neg \psi \rightarrow (\chi \wedge \psi \leftrightarrow \neg \varphi) \)
Proof
l0
simpr
niabn.1
pm2.24i _
pm5.21ni l0 _