Theorem nic-idbl

Double the terms. Since doubling is the same as negation, this can be viewed as a contraposition inference. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypothesis
nic-idbl.1
\( \vdash \varphi \barwedge (\psi \barwedge \psi) \)
Conclusion
\( \vdash (\psi \barwedge \psi) \barwedge ((\varphi \barwedge \varphi) \barwedge (\varphi \barwedge \varphi)) \)
Proof
nic-idbl.1
\( \vdash \varphi \barwedge (\psi \barwedge \psi) \)
l1
nic-imp _
\( \vdash (\psi \barwedge \psi) \barwedge ((\varphi \barwedge \psi) \barwedge (\varphi \barwedge \psi)) \)
nic-idbl.1
\( \vdash \varphi \barwedge (\psi \barwedge \psi) \)
nic-imp _
\( \vdash (\varphi \barwedge \psi) \barwedge ((\varphi \barwedge \varphi) \barwedge (\varphi \barwedge \varphi)) \)
nic-ich l1 _