Theorem luklem6

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

Proof

Step	Hyp	Ref	Expression
1		luk-1	|- ( ( ph -> ( ph -> ps ) ) -> ( ( ( ph -> ps ) -> ps ) -> ( ph -> ps ) ) )
2		luklem5	|- ( -. ( ph -> ps ) -> ( -. ps -> -. ( ph -> ps ) ) )
3		luklem2	|- ( ( -. ps -> -. ( ph -> ps ) ) -> ( ( ( -. ps -> ps ) -> ps ) -> ( ( ph -> ps ) -> ps ) ) )
4		luklem4	|- ( ( ( ( -. ps -> ps ) -> ps ) -> ( ( ph -> ps ) -> ps ) ) -> ( ( ph -> ps ) -> ps ) )
5	3 4	luklem1	|- ( ( -. ps -> -. ( ph -> ps ) ) -> ( ( ph -> ps ) -> ps ) )
6	2 5	luklem1	|- ( -. ( ph -> ps ) -> ( ( ph -> ps ) -> ps ) )
7		luk-1	|- ( ( -. ( ph -> ps ) -> ( ( ph -> ps ) -> ps ) ) -> ( ( ( ( ph -> ps ) -> ps ) -> ( ph -> ps ) ) -> ( -. ( ph -> ps ) -> ( ph -> ps ) ) ) )
8	6 7	ax-mp	|- ( ( ( ( ph -> ps ) -> ps ) -> ( ph -> ps ) ) -> ( -. ( ph -> ps ) -> ( ph -> ps ) ) )
9		luk-1	|- ( ( ( ( ( ph -> ps ) -> ps ) -> ( ph -> ps ) ) -> ( -. ( ph -> ps ) -> ( ph -> ps ) ) ) -> ( ( ( -. ( ph -> ps ) -> ( ph -> ps ) ) -> ( ph -> ps ) ) -> ( ( ( ( ph -> ps ) -> ps ) -> ( ph -> ps ) ) -> ( ph -> ps ) ) ) )
10	8 9	ax-mp	|- ( ( ( -. ( ph -> ps ) -> ( ph -> ps ) ) -> ( ph -> ps ) ) -> ( ( ( ( ph -> ps ) -> ps ) -> ( ph -> ps ) ) -> ( ph -> ps ) ) )
11		luklem4	|- ( ( ( ( -. ( ph -> ps ) -> ( ph -> ps ) ) -> ( ph -> ps ) ) -> ( ( ( ( ph -> ps ) -> ps ) -> ( ph -> ps ) ) -> ( ph -> ps ) ) ) -> ( ( ( ( ph -> ps ) -> ps ) -> ( ph -> ps ) ) -> ( ph -> ps ) ) )
12	10 11	ax-mp	|- ( ( ( ( ph -> ps ) -> ps ) -> ( ph -> ps ) ) -> ( ph -> ps ) )
13	1 12	luklem1	|- ( ( ph -> ( ph -> ps ) ) -> ( ph -> ps ) )