Theorem nic-luk2

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

Conclusion
\( \vdash (\neg \varphi \rightarrow \varphi) \rightarrow \varphi \)
Proof
nic-dfim
l1
nic-bi2 _
\( \vdash (\neg \varphi \rightarrow \varphi) \barwedge ((\neg \varphi \barwedge (\varphi \barwedge \varphi)) \barwedge (\neg \varphi \barwedge (\varphi \barwedge \varphi))) \)
l2
nic-dfneg
\( \vdash ((\varphi \barwedge \varphi) \barwedge \neg \varphi) \barwedge (((\varphi \barwedge \varphi) \barwedge (\varphi \barwedge \varphi)) \barwedge (\neg \varphi \barwedge \neg \varphi)) \)
nic-id
\( \vdash (\varphi \barwedge \varphi) \barwedge ((\varphi \barwedge \varphi) \barwedge (\varphi \barwedge \varphi)) \)
nic-iimp1 l2 _
nic-isw2 _
\( \vdash (\varphi \barwedge \varphi) \barwedge (\neg \varphi \barwedge (\varphi \barwedge \varphi)) \)
nic-iimp1 l1 _
l7
nic-isw1 _
\( \vdash (\neg \varphi \rightarrow \varphi) \barwedge (\varphi \barwedge \varphi) \)
nic-dfim
nic-bi1 _
\( \vdash ((\neg \varphi \rightarrow \varphi) \barwedge (\varphi \barwedge \varphi)) \barwedge (((\neg \varphi \rightarrow \varphi) \rightarrow \varphi) \barwedge ((\neg \varphi \rightarrow \varphi) \rightarrow \varphi)) \)
nic-mp l7 _