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

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