Theorem nic-iimp2

Inference version of nic-imp using left-handed term. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses
nic-iimp2.1
\( \vdash (\varphi \barwedge \psi) \barwedge (\chi \barwedge \chi) \)
nic-iimp2.2
\( \vdash \theta \barwedge \varphi \)
Conclusion
\( \vdash \theta \barwedge (\chi \barwedge \chi) \)
Proof
nic-iimp2.1
l1
nic-isw1 _
\( \vdash (\chi \barwedge \chi) \barwedge (\varphi \barwedge \psi) \)
nic-iimp2.2
\( \vdash \theta \barwedge \varphi \)
nic-iimp1 l1 _