Theorem nic-mp

Derive Nicod's rule of modus ponens using 'nand', from the standard one. Although the major and minor premise together also imply \( \chi \), this form is necessary for useful derivations from nic-ax. In a pure (standalone) treatment of Nicod's axiom, this theorem would be changed to an axiom ($a statement). (Contributed by Jeff Hoffman, 19-Nov-2007.) (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) \)
nannan
\( \vdash \varphi \barwedge (\chi \barwedge \psi) \leftrightarrow \varphi \rightarrow \chi \wedge \psi \)
mpbi l1 _
\( \vdash \varphi \rightarrow \chi \wedge \psi \)
simprd _
\( \vdash \varphi \rightarrow \psi \)
ax-mp l0 _