Theorem looinv

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

	Ref	Expression
Assertion	looinv	|- ( ( ( ph -> ps ) -> ps ) -> ( ( ps -> ph ) -> ph ) )

Proof

Step	Hyp	Ref	Expression
1		imim1	|- ( ( ( ph -> ps ) -> ps ) -> ( ( ps -> ph ) -> ( ( ph -> ps ) -> ph ) ) )
2		peirce	|- ( ( ( ph -> ps ) -> ph ) -> ph )
3	1 2	syl6	|- ( ( ( ph -> ps ) -> ps ) -> ( ( ps -> ph ) -> ph ) )