Theorem nic-imp

Inference for nic-mp using nic-ax as major premise. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypothesis
nic-imp.1
\( \vdash \varphi \barwedge (\chi \barwedge \psi) \)
Conclusion
\( \vdash (\theta \barwedge \chi) \barwedge ((\varphi \barwedge \theta) \barwedge (\varphi \barwedge \theta)) \)
Proof
l0
nic-imp.1
\( \vdash \varphi \barwedge (\chi \barwedge \psi) \)
nic-ax
\( \vdash (\varphi \barwedge (\chi \barwedge \psi)) \barwedge ((\varphi \barwedge (\varphi \barwedge \varphi)) \barwedge ((\theta \barwedge \chi) \barwedge ((\varphi \barwedge \theta) \barwedge (\varphi \barwedge \theta)))) \)
nic-mp l0 _