Theorem nic-isw1

Inference version of nic-swap. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypothesis
nic-isw1.1
\( \vdash \theta \barwedge \varphi \)
Conclusion
\( \vdash \varphi \barwedge \theta \)
Proof
l0
nic-isw1.1
\( \vdash \theta \barwedge \varphi \)
nic-swap
\( \vdash (\theta \barwedge \varphi) \barwedge ((\varphi \barwedge \theta) \barwedge (\varphi \barwedge \theta)) \)
nic-mp l0 _