Theorem nic-luk1

Proof of luk-1 from nic-ax and nic-mp (and Definitions nic-dfim and nic-dfneg ). Note that the standard axioms [ax-1], [ax-2], and [ax-3] are proved from the Lukasiewicz axioms by Theorems ax1, ax2, and ax3. (Contributed by Jeff Hoffman, 18-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)

Conclusion
\( \vdash (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
Proof
nic-dfim
l1
nic-bi2 _
\( \vdash (\varphi \rightarrow \psi) \barwedge ((\varphi \barwedge (\psi \barwedge \psi)) \barwedge (\varphi \barwedge (\psi \barwedge \psi))) \)
nic-ax
nic-isw2 _
\( \vdash (\varphi \barwedge (\psi \barwedge \psi)) \barwedge ((((\chi \barwedge \chi) \barwedge \psi) \barwedge ((\varphi \barwedge (\chi \barwedge \chi)) \barwedge (\varphi \barwedge (\chi \barwedge \chi)))) \barwedge (\varphi \barwedge (\varphi \barwedge \varphi))) \)
l4
nic-idel _
\( \vdash (\varphi \barwedge (\psi \barwedge \psi)) \barwedge ((((\chi \barwedge \chi) \barwedge \psi) \barwedge ((\varphi \barwedge (\chi \barwedge \chi)) \barwedge (\varphi \barwedge (\chi \barwedge \chi)))) \barwedge (((\chi \barwedge \chi) \barwedge \psi) \barwedge ((\varphi \barwedge (\chi \barwedge \chi)) \barwedge (\varphi \barwedge (\chi \barwedge \chi))))) \)
nic-dfim
nic-bi1 _
nic-idbl _
\( \vdash ((\varphi \rightarrow \chi) \barwedge (\varphi \rightarrow \chi)) \barwedge (((\varphi \barwedge (\chi \barwedge \chi)) \barwedge (\varphi \barwedge (\chi \barwedge \chi))) \barwedge ((\varphi \barwedge (\chi \barwedge \chi)) \barwedge (\varphi \barwedge (\chi \barwedge \chi)))) \)
l8
nic-imp _
\( \vdash (((\chi \barwedge \chi) \barwedge \psi) \barwedge ((\varphi \barwedge (\chi \barwedge \chi)) \barwedge (\varphi \barwedge (\chi \barwedge \chi)))) \barwedge ((((\varphi \rightarrow \chi) \barwedge (\varphi \rightarrow \chi)) \barwedge ((\chi \barwedge \chi) \barwedge \psi)) \barwedge (((\varphi \rightarrow \chi) \barwedge (\varphi \rightarrow \chi)) \barwedge ((\chi \barwedge \chi) \barwedge \psi))) \)
nic-dfim
l10
nic-bi2 _
\( \vdash (\psi \rightarrow \chi) \barwedge ((\psi \barwedge (\chi \barwedge \chi)) \barwedge (\psi \barwedge (\chi \barwedge \chi))) \)
nic-swap
\( \vdash (\psi \barwedge (\chi \barwedge \chi)) \barwedge (((\chi \barwedge \chi) \barwedge \psi) \barwedge ((\chi \barwedge \chi) \barwedge \psi)) \)
nic-ich l10 _
\( \vdash (\psi \rightarrow \chi) \barwedge (((\chi \barwedge \chi) \barwedge \psi) \barwedge ((\chi \barwedge \chi) \barwedge \psi)) \)
nic-imp _
\( \vdash (((\varphi \rightarrow \chi) \barwedge (\varphi \rightarrow \chi)) \barwedge ((\chi \barwedge \chi) \barwedge \psi)) \barwedge (((\psi \rightarrow \chi) \barwedge ((\varphi \rightarrow \chi) \barwedge (\varphi \rightarrow \chi))) \barwedge ((\psi \rightarrow \chi) \barwedge ((\varphi \rightarrow \chi) \barwedge (\varphi \rightarrow \chi)))) \)
nic-ich l8 _
\( \vdash (((\chi \barwedge \chi) \barwedge \psi) \barwedge ((\varphi \barwedge (\chi \barwedge \chi)) \barwedge (\varphi \barwedge (\chi \barwedge \chi)))) \barwedge (((\psi \rightarrow \chi) \barwedge ((\varphi \rightarrow \chi) \barwedge (\varphi \rightarrow \chi))) \barwedge ((\psi \rightarrow \chi) \barwedge ((\varphi \rightarrow \chi) \barwedge (\varphi \rightarrow \chi)))) \)
l15
nic-ich l4 _
\( \vdash (\varphi \barwedge (\psi \barwedge \psi)) \barwedge (((\psi \rightarrow \chi) \barwedge ((\varphi \rightarrow \chi) \barwedge (\varphi \rightarrow \chi))) \barwedge ((\psi \rightarrow \chi) \barwedge ((\varphi \rightarrow \chi) \barwedge (\varphi \rightarrow \chi)))) \)
nic-dfim
nic-bi1 _
\( \vdash ((\psi \rightarrow \chi) \barwedge ((\varphi \rightarrow \chi) \barwedge (\varphi \rightarrow \chi))) \barwedge (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \barwedge ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi)) \)
nic-ich l15 _
\( \vdash (\varphi \barwedge (\psi \barwedge \psi)) \barwedge (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \barwedge ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi)) \)
l19
nic-ich l1 _
\( \vdash (\varphi \rightarrow \psi) \barwedge (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \barwedge ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi)) \)
nic-dfim
nic-bi1 _
\( \vdash ((\varphi \rightarrow \psi) \barwedge (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \barwedge ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi))) \barwedge (((\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \barwedge ((\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi)) \)
nic-mp l19 _