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 ( ( ( 𝜑𝜓 ) → 𝜓 ) → ( ( 𝜓𝜑 ) → 𝜑 ) )

Proof

Step Hyp Ref Expression
1 imim1 ( ( ( 𝜑𝜓 ) → 𝜓 ) → ( ( 𝜓𝜑 ) → ( ( 𝜑𝜓 ) → 𝜑 ) ) )
2 peirce ( ( ( 𝜑𝜓 ) → 𝜑 ) → 𝜑 )
3 1 2 syl6 ( ( ( 𝜑𝜓 ) → 𝜓 ) → ( ( 𝜓𝜑 ) → 𝜑 ) )