Theorem luk-1 1420

Description: 1 of 3 axioms for propositional calculus due to Lukasiewicz, derived from Meredith's sole axiom. (Contributed by NM, 14-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
luk-1	|- ((ph -> ps) -> ((ps -> ch) -> (ph -> ch)))

Proof of Theorem luk-1

Step	Hyp	Ref	Expression
1		ax-meredith 1406	. 2 |- (((((ch -> ch) -> (-. -. -. ph -> -. ph)) -> -. -. ph) -> ps) -> ((ps -> ch) -> (ph -> ch)))
2		merlem13 1419	. . . 4 |- ((ph -> ps) -> ((((ch -> ch) -> (-. -. -. ph -> -. ph)) -> -. -. ph) -> ps))
3		merlem13 1419	. . . 4 |- (((ph -> ps) -> ((((ch -> ch) -> (-. -. -. ph -> -. ph)) -> -. -. ph) -> ps)) -> ((((((ps -> ch) -> (ph -> ch)) -> ph) -> (-. -. -. (ph -> ps) -> -. (ph -> ps))) -> -. -. (ph -> ps)) -> ((((ch -> ch) -> (-. -. -. ph -> -. ph)) -> -. -. ph) -> ps)))
4	2, 3	ax-mp 5	. . 3 |- ((((((ps -> ch) -> (ph -> ch)) -> ph) -> (-. -. -. (ph -> ps) -> -. (ph -> ps))) -> -. -. (ph -> ps)) -> ((((ch -> ch) -> (-. -. -. ph -> -. ph)) -> -. -. ph) -> ps))
5		ax-meredith 1406	. . 3 |- (((((((ps -> ch) -> (ph -> ch)) -> ph) -> (-. -. -. (ph -> ps) -> -. (ph -> ps))) -> -. -. (ph -> ps)) -> ((((ch -> ch) -> (-. -. -. ph -> -. ph)) -> -. -. ph) -> ps)) -> ((((((ch -> ch) -> (-. -. -. ph -> -. ph)) -> -. -. ph) -> ps) -> ((ps -> ch) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch)))))
6	4, 5	ax-mp 5	. 2 |- ((((((ch -> ch) -> (-. -. -. ph -> -. ph)) -> -. -. ph) -> ps) -> ((ps -> ch) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))
7	1, 6	ax-mp 5	1 |- ((ph -> ps) -> ((ps -> ch) -> (ph -> ch)))

Syntax hints:  -. wn 3   -> wi 4

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

This theorem is referenced by:  luklem1  1423  luklem2  1424  luklem4  1426  luklem6  1428  luklem7  1429  luklem8  1430