Theorem luklem6 1428

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

Assertion

Ref	Expression
luklem6	|- ((ph -> (ph -> ps)) -> (ph -> ps))

Proof of Theorem luklem6

Step	Hyp	Ref	Expression
1		luk-1 1420	. 2 |- ((ph -> (ph -> ps)) -> (((ph -> ps) -> ps) -> (ph -> ps)))
2		luklem5 1427	. . . . . 6 |- (-. (ph -> ps) -> (-. ps -> -. (ph -> ps)))
3		luklem2 1424	. . . . . . 7 |- ((-. ps -> -. (ph -> ps)) -> (((-. ps -> ps) -> ps) -> ((ph -> ps) -> ps)))
4		luklem4 1426	. . . . . . 7 |- ((((-. ps -> ps) -> ps) -> ((ph -> ps) -> ps)) -> ((ph -> ps) -> ps))
5	3, 4	luklem1 1423	. . . . . 6 |- ((-. ps -> -. (ph -> ps)) -> ((ph -> ps) -> ps))
6	2, 5	luklem1 1423	. . . . 5 |- (-. (ph -> ps) -> ((ph -> ps) -> ps))
7		luk-1 1420	. . . . 5 |- ((-. (ph -> ps) -> ((ph -> ps) -> ps)) -> ((((ph -> ps) -> ps) -> (ph -> ps)) -> (-. (ph -> ps) -> (ph -> ps))))
8	6, 7	ax-mp 5	. . . 4 |- ((((ph -> ps) -> ps) -> (ph -> ps)) -> (-. (ph -> ps) -> (ph -> ps)))
9		luk-1 1420	. . . 4 |- (((((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 5	. . 3 |- (((-. (ph -> ps) -> (ph -> ps)) -> (ph -> ps)) -> ((((ph -> ps) -> ps) -> (ph -> ps)) -> (ph -> ps)))
11		luklem4 1426	. . 3 |- ((((-. (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 5	. 2 |- ((((ph -> ps) -> ps) -> (ph -> ps)) -> (ph -> ps))
13	1, 12	luklem1 1423	1 |- ((ph -> (ph -> ps)) -> (ph -> ps))

Syntax hints:  -. wn 3   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-meredith 1406

This theorem is referenced by:  luklem7  1429  ax2  1432