Metamath Proof Explorer

Theorem impsingle

Description: The shortest single axiom for implicational calculus, due to Lukasiewicz. It is now known to be theunique shortest axiom. The axiom is proved here starting from { ax-1 , ax-2 and peirce }. (Contributed by Larry Lesyna and Jeffrey P. Machado, 18-Jul-2023) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	impsingle	$⊢ ((φ \to ψ) \to χ) \to ((χ \to φ) \to (θ \to φ))$

Proof

Step	Hyp	Ref	Expression
1		imim1	$⊢ ((φ \to ψ) \to χ) \to ((χ \to φ) \to ((φ \to ψ) \to φ))$
2		peirce	$⊢ ((φ \to ψ) \to φ) \to φ$
3	2	a1d	$⊢ ((φ \to ψ) \to φ) \to (θ \to φ)$
4	1 3	syl6	$⊢ ((φ \to ψ) \to χ) \to ((χ \to φ) \to (θ \to φ))$