Theorem nic-isw2

Inference for swapping nested terms. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)

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