Theorem nic-mpALT

A direct proof of nic-mp. (Contributed by NM, 30-Dec-2008.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses
nic-jmin
\( \vdash \varphi \)
nic-jmaj
\( \vdash \varphi \barwedge (\chi \barwedge \psi) \)
Conclusion
\( \vdash \psi \)
Proof
l0
nic-jmin
\( \vdash \varphi \)
l1
nic-jmaj
\( \vdash \varphi \barwedge (\chi \barwedge \psi) \)
l2
df-nan
\( \vdash \varphi \barwedge (\chi \barwedge \psi) \leftrightarrow \neg (\varphi \wedge (\chi \barwedge \psi)) \)
df-nan
anbi2i _
\( \vdash \varphi \wedge (\chi \barwedge \psi) \leftrightarrow \varphi \wedge \neg (\chi \wedge \psi) \)
xchbinx l2 _
\( \vdash \varphi \barwedge (\chi \barwedge \psi) \leftrightarrow \neg (\varphi \wedge \neg (\chi \wedge \psi)) \)
l6
mpbi l1 _
\( \vdash \neg (\varphi \wedge \neg (\chi \wedge \psi)) \)
iman
\( \vdash \varphi \rightarrow \chi \wedge \psi \leftrightarrow \neg (\varphi \wedge \neg (\chi \wedge \psi)) \)
mpbir l6 _
\( \vdash \varphi \rightarrow \chi \wedge \psi \)
simprd _
\( \vdash \varphi \rightarrow \psi \)
ax-mp l0 _