Theorem looinv

The Inversion Axiom of the infinite-valued sentential logic (L-infinity) of Lukasiewicz. Using dfor2, we can see that this essentially expresses "disjunction is commutative". Theorem *2.69 of [WhiteheadRussell] p. 108. It is a special instance of the axiom "Roll", see peirceroll. (Contributed by NM, 12-Aug-2004.)

Conclusion
\( \vdash ((\varphi \rightarrow \psi) \rightarrow \psi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \varphi \)
Proof
l0
imim1
\( \vdash ((\varphi \rightarrow \psi) \rightarrow \psi) \rightarrow (\psi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \)
peirce
\( \vdash ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \varphi \)
syl6 l0 _