Theorem luklem6 948

Description: Used to rederive 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 940	. 2 |- ((ph -> (ph -> ps)) -> (((ph -> ps) -> ps) -> (ph -> ps)))
2		luklem5 947	. . . . . 6 |- (-. (ph -> ps) -> (-. ps -> -. (ph -> ps)))
3		luklem2 944	. . . . . . 7 |- ((-. ps -> -. (ph -> ps)) -> (((-. ps -> ps) -> ps) -> ((ph -> ps) -> ps)))
4		luklem4 946	. . . . . . 7 |- ((((-. ps -> ps) -> ps) -> ((ph -> ps) -> ps)) -> ((ph -> ps) -> ps))
5	3, 4	luklem1 943	. . . . . 6 |- ((-. ps -> -. (ph -> ps)) -> ((ph -> ps) -> ps))
6	2, 5	luklem1 943	. . . . 5 |- (-. (ph -> ps) -> ((ph -> ps) -> ps))
7		luk-1 940	. . . . 5 |- ((-. (ph -> ps) -> ((ph -> ps) -> ps)) -> ((((ph -> ps) -> ps) -> (ph -> ps)) -> (-. (ph -> ps) -> (ph -> ps))))
8	6, 7	ax-mp 7	. . . 4 |- ((((ph -> ps) -> ps) -> (ph -> ps)) -> (-. (ph -> ps) -> (ph -> ps)))
9		luk-1 940	. . . 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 7	. . 3 |- (((-. (ph -> ps) -> (ph -> ps)) -> (ph -> ps)) -> ((((ph -> ps) -> ps) -> (ph -> ps)) -> (ph -> ps)))
11		luklem4 946	. . 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 7	. 2 |- ((((ph -> ps) -> ps) -> (ph -> ps)) -> (ph -> ps))
13	1, 12	luklem1 943	1 |- ((ph -> (ph -> ps)) -> (ph -> ps))

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  luklem7 949  ax2 952

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

Copyright terms: Public domain