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

Proof

Step	Hyp	Ref	Expression
1		imim1	⊢ ( ( ( 𝜑 → 𝜓 ) → 𝜒 ) → ( ( 𝜒 → 𝜑 ) → ( ( 𝜑 → 𝜓 ) → 𝜑 ) ) )
2		peirce	⊢ ( ( ( 𝜑 → 𝜓 ) → 𝜑 ) → 𝜑 )
3	2	a1d	⊢ ( ( ( 𝜑 → 𝜓 ) → 𝜑 ) → ( 𝜃 → 𝜑 ) )
4	1 3	syl6	⊢ ( ( ( 𝜑 → 𝜓 ) → 𝜒 ) → ( ( 𝜒 → 𝜑 ) → ( 𝜃 → 𝜑 ) ) )