Theorem nic-iimp1

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

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