Theorem luklem6 666

Description: Lemma for rederiving standard propositional axioms from Lukasiewicz'.

Assertion

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

Proof of Theorem luklem6

Step	Hyp	Ref	Expression
1		luk-1 658	. 2 |- ((ph -> (ph -> ps)) -> (((ph -> ps) -> ps) -> (ph -> ps)))
2		luklem5 665	. . . . . 6 |- (-. (ph -> ps) -> (-. ps -> -. (ph -> ps)))
3		luklem2 662	. . . . . . 7 |- ((-. ps -> -. (ph -> ps)) -> (((-. ps -> ps) -> ps) -> ((ph -> ps) -> ps)))
4		luklem4 664	. . . . . . 7 |- ((((-. ps -> ps) -> ps) -> ((ph -> ps) -> ps)) -> ((ph -> ps) -> ps))
5	3, 4	luklem1 661	. . . . . 6 |- ((-. ps -> -. (ph -> ps)) -> ((ph -> ps) -> ps))
6	2, 5	luklem1 661	. . . . 5 |- (-. (ph -> ps) -> ((ph -> ps) -> ps))
7		luk-1 658	. . . . 5 |- ((-. (ph -> ps) -> ((ph -> ps) -> ps)) -> ((((ph -> ps) -> ps) -> (ph -> ps)) -> (-. (ph -> ps) -> (ph -> ps))))
8	6, 7	ax-mp 6	. . . 4 |- ((((ph -> ps) -> ps) -> (ph -> ps)) -> (-. (ph -> ps) -> (ph -> ps)))
9		luk-1 658	. . . 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 6	. . 3 |- (((-. (ph -> ps) -> (ph -> ps)) -> (ph -> ps)) -> ((((ph -> ps) -> ps) -> (ph -> ps)) -> (ph -> ps)))
11		luklem4 664	. . 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 6	. 2 |- ((((ph -> ps) -> ps) -> (ph -> ps)) -> (ph -> ps))
13	1, 12	luklem1 661	1 |- ((ph -> (ph -> ps)) -> (ph -> ps))

Syntax hints:  -. wn 1   -> wi 2

This theorem is referenced by:  luklem7 667  ax2 670

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

metamath.org