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

Proof

Step	Hyp	Ref	Expression
1		imim1	|- ( ( ( ph -> ps ) -> ch ) -> ( ( ch -> ph ) -> ( ( ph -> ps ) -> ph ) ) )
2		peirce	|- ( ( ( ph -> ps ) -> ph ) -> ph )
3	2	a1d	|- ( ( ( ph -> ps ) -> ph ) -> ( th -> ph ) )
4	1 3	syl6	|- ( ( ( ph -> ps ) -> ch ) -> ( ( ch -> ph ) -> ( th -> ph ) ) )