This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ ((φ \to ψ) \to ψ) \to ((ψ \to φ) \to φ)$

Proof

Step	Hyp	Ref	Expression
1		imim1	$⊢ ((φ \to ψ) \to ψ) \to ((ψ \to φ) \to ((φ \to ψ) \to φ))$
2		peirce	$⊢ ((φ \to ψ) \to φ) \to φ$
3	1 2	syl6	$⊢ ((φ \to ψ) \to ψ) \to ((ψ \to φ) \to φ)$