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	|- ( ( ( ( ph -> ps ) -> ph ) -> ph ) -> ( ( ( ph -> ps ) -> ch ) -> ( ( ch -> ph ) -> ph ) ) )

Proof

Step	Hyp	Ref	Expression
1		imim1	|- ( ( ( ph -> ps ) -> ch ) -> ( ( ch -> ph ) -> ( ( ph -> ps ) -> ph ) ) )
2		id	|- ( ( ( ( ph -> ps ) -> ph ) -> ph ) -> ( ( ( ph -> ps ) -> ph ) -> ph ) )
3	1 2	syl9r	|- ( ( ( ( ph -> ps ) -> ph ) -> ph ) -> ( ( ( ph -> ps ) -> ch ) -> ( ( ch -> ph ) -> ph ) ) )