Theorem nic-luk3

Proof of luk-3 from nic-ax and nic-mp. (Contributed by Jeff Hoffman, 18-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)

Conclusion
\( \vdash \varphi \rightarrow \neg \varphi \rightarrow \psi \)
Proof
nic-dfim
l1
nic-bi1 _
\( \vdash (\neg \varphi \barwedge (\psi \barwedge \psi)) \barwedge ((\neg \varphi \rightarrow \psi) \barwedge (\neg \varphi \rightarrow \psi)) \)
nic-dfneg
l3
nic-bi2 _
\( \vdash \neg \varphi \barwedge ((\varphi \barwedge \varphi) \barwedge (\varphi \barwedge \varphi)) \)
nic-id
\( \vdash \varphi \barwedge (\varphi \barwedge \varphi) \)
nic-iimp1 l3 _
\( \vdash \varphi \barwedge \neg \varphi \)
l6
nic-iimp2 l1 _
\( \vdash \varphi \barwedge ((\neg \varphi \rightarrow \psi) \barwedge (\neg \varphi \rightarrow \psi)) \)
nic-dfim
nic-bi1 _
\( \vdash (\varphi \barwedge ((\neg \varphi \rightarrow \psi) \barwedge (\neg \varphi \rightarrow \psi))) \barwedge ((\varphi \rightarrow \neg \varphi \rightarrow \psi) \barwedge (\varphi \rightarrow \neg \varphi \rightarrow \psi)) \)
nic-mp l6 _