Theorem nic-stdmp

Derive the standard modus ponens from nic-mp. (Contributed by Jeff Hoffman, 18-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses
nic-smin
\( \vdash \varphi \)
nic-smaj
\( \vdash \varphi \rightarrow \psi \)
Conclusion
\( \vdash \psi \)
Proof
l0
nic-smin
\( \vdash \varphi \)
l1
nic-smaj
\( \vdash \varphi \rightarrow \psi \)
nic-dfim
nic-bi2 _
\( \vdash (\varphi \rightarrow \psi) \barwedge ((\varphi \barwedge (\psi \barwedge \psi)) \barwedge (\varphi \barwedge (\psi \barwedge \psi))) \)
nic-mp l1 _
\( \vdash \varphi \barwedge (\psi \barwedge \psi) \)
nic-mp l0 _