Theorem luklem1

Description: Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 23-Dec-2002) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	luklem1.1	|- ( ph -> ps )
	luklem1.2	|- ( ps -> ch )
Assertion	luklem1	|- ( ph -> ch )

Proof

Step	Hyp	Ref	Expression
1		luklem1.1	|- ( ph -> ps )
2		luklem1.2	|- ( ps -> ch )
3		luk-1	|- ( ( ph -> ps ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) )
4	1 3	ax-mp	|- ( ( ps -> ch ) -> ( ph -> ch ) )
5	2 4	ax-mp	|- ( ph -> ch )