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	$⊢ (((φ \to ψ) \to φ) \to φ) \to (((φ \to ψ) \to χ) \to ((χ \to φ) \to φ))$

Proof

Step	Hyp	Ref	Expression
1		imim1	$⊢ ((φ \to ψ) \to χ) \to ((χ \to φ) \to ((φ \to ψ) \to φ))$
2		id	$⊢ (((φ \to ψ) \to φ) \to φ) \to (((φ \to ψ) \to φ) \to φ)$
3	1 2	syl9r	$⊢ (((φ \to ψ) \to φ) \to φ) \to (((φ \to ψ) \to χ) \to ((χ \to φ) \to φ))$