Theorem nic-bi2

Inference to extract the other side of an implication from a 'biconditional' definition. (Contributed by Jeff Hoffman, 18-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypothesis
nic-bi2.1
\( \vdash (\varphi \barwedge \psi) \barwedge ((\varphi \barwedge \varphi) \barwedge (\psi \barwedge \psi)) \)
Conclusion
\( \vdash \psi \barwedge (\varphi \barwedge \varphi) \)
Proof
nic-bi2.1
l1
nic-isw2 _
\( \vdash (\varphi \barwedge \psi) \barwedge ((\psi \barwedge \psi) \barwedge (\varphi \barwedge \varphi)) \)
nic-id
\( \vdash \psi \barwedge (\psi \barwedge \psi) \)
nic-iimp1 l1 _
\( \vdash \psi \barwedge (\varphi \barwedge \psi) \)
nic-idel _