Theorem peirceroll 85

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

Assertion

Ref	Expression
peirceroll	|- ( ( ( ( ph -> ps ) -> ph ) -> ph ) -> ( ( ( ph -> ps ) -> ch ) -> ( ( ch -> ph ) -> ph ) ) )

Proof of Theorem peirceroll

Step	Hyp	Ref	Expression
1		imim1 83	. 2 |- ( ( ( ph -> ps ) -> ch ) -> ( ( ch -> ph ) -> ( ( ph -> ps ) -> ph ) ) )
2		imim2 58	. 2 |- ( ( ( ( ph -> ps ) -> ph ) -> ph ) -> ( ( ( ch -> ph ) -> ( ( ph -> ps ) -> ph ) ) -> ( ( ch -> ph ) -> ph ) ) )
3	1, 2	syl5 34	1 |- ( ( ( ( ph -> ps ) -> ph ) -> ph ) -> ( ( ( ph -> ps ) -> ch ) -> ( ( ch -> ph ) -> ph ) ) )

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  bj-peircecurry  32545