Metamath Proof Explorer


Theorem peirceroll

Description: Over minimal implicational calculus, Peirce's axiom peirce implies an axiom sometimes called "Roll", ( ( ( ph -> ps ) -> ch ) -> ( ( ch -> ph ) -> ph ) ) , of which looinv is a special instance. The converse also holds: substitute ( ph -> ps ) for ch in Roll and use id and ax-mp . (Contributed by BJ, 15-Jun-2021)

Ref Expression
Assertion peirceroll ( ( ( ( 𝜑𝜓 ) → 𝜑 ) → 𝜑 ) → ( ( ( 𝜑𝜓 ) → 𝜒 ) → ( ( 𝜒𝜑 ) → 𝜑 ) ) )

Proof

Step Hyp Ref Expression
1 imim1 ( ( ( 𝜑𝜓 ) → 𝜒 ) → ( ( 𝜒𝜑 ) → ( ( 𝜑𝜓 ) → 𝜑 ) ) )
2 id ( ( ( ( 𝜑𝜓 ) → 𝜑 ) → 𝜑 ) → ( ( ( 𝜑𝜓 ) → 𝜑 ) → 𝜑 ) )
3 1 2 syl9r ( ( ( ( 𝜑𝜓 ) → 𝜑 ) → 𝜑 ) → ( ( ( 𝜑𝜓 ) → 𝜒 ) → ( ( 𝜒𝜑 ) → 𝜑 ) ) )