Theorem minimp-ax2
Derivation of [ax-2] from [ax-mp] and minimp. (Contributed by BJ,
4-Apr-2021.) (Proof modification is discouraged.)
(New usage is discouraged.)
Conclusion
\( \vdash (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi \)
Proof
l0
minimp-ax2c
\( \vdash (\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l1
minimp-ax2c
\( \vdash ((\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi \)
minimp-syllsimp
\( \vdash (((\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi \)
l3
ax-mp l1 _
\( \vdash (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi \)
l4
minimp-ax2c
\( \vdash ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi \)
minimp-syllsimp
\( \vdash (((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi \)
ax-mp l4 _
\( \vdash ((\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi \)
mp2 l0 l3 _