Theorem luklem2

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

	Ref	Expression
Assertion	luklem2	|- ( ( ph -> -. ps ) -> ( ( ( ph -> ch ) -> th ) -> ( ps -> th ) ) )

Proof

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