Theorem merlem5 1411

Description: Step 11 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (Contributed by NM, 14-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
merlem5	|- ((ph -> ps) -> (-. -. ph -> ps))

Proof of Theorem merlem5

Step	Hyp	Ref	Expression
1		ax-meredith 1406	. 2 |- (((((ps -> ps) -> (-. ps -> -. ps)) -> ps) -> ps) -> ((ps -> ps) -> (ps -> ps)))
2		ax-meredith 1406	. . 3 |- (((((ps -> ps) -> (-. ps -> -. -. -. ph)) -> ps) -> ph) -> ((ph -> ps) -> (-. -. ph -> ps)))
3		merlem1 1407	. . . . 5 |- ((((ph -> ps) -> (-. -. ph -> ps)) -> -. (((((ps -> ps) -> (-. ps -> -. ps)) -> ps) -> ps) -> ((ps -> ps) -> (ps -> ps)))) -> (-. ph -> -. (((((ps -> ps) -> (-. ps -> -. ps)) -> ps) -> ps) -> ((ps -> ps) -> (ps -> ps)))))
4		merlem4 1410	. . . . 5 |- (((((ph -> ps) -> (-. -. ph -> ps)) -> -. (((((ps -> ps) -> (-. ps -> -. ps)) -> ps) -> ps) -> ((ps -> ps) -> (ps -> ps)))) -> (-. ph -> -. (((((ps -> ps) -> (-. ps -> -. ps)) -> ps) -> ps) -> ((ps -> ps) -> (ps -> ps))))) -> ((((((ph -> ps) -> (-. -. ph -> ps)) -> -. (((((ps -> ps) -> (-. ps -> -. ps)) -> ps) -> ps) -> ((ps -> ps) -> (ps -> ps)))) -> (-. ph -> -. (((((ps -> ps) -> (-. ps -> -. ps)) -> ps) -> ps) -> ((ps -> ps) -> (ps -> ps))))) -> ph) -> ((((ps -> ps) -> (-. ps -> -. -. -. ph)) -> ps) -> ph)))
5	3, 4	ax-mp 5	. . . 4 |- ((((((ph -> ps) -> (-. -. ph -> ps)) -> -. (((((ps -> ps) -> (-. ps -> -. ps)) -> ps) -> ps) -> ((ps -> ps) -> (ps -> ps)))) -> (-. ph -> -. (((((ps -> ps) -> (-. ps -> -. ps)) -> ps) -> ps) -> ((ps -> ps) -> (ps -> ps))))) -> ph) -> ((((ps -> ps) -> (-. ps -> -. -. -. ph)) -> ps) -> ph))
6		ax-meredith 1406	. . . 4 |- (((((((ph -> ps) -> (-. -. ph -> ps)) -> -. (((((ps -> ps) -> (-. ps -> -. ps)) -> ps) -> ps) -> ((ps -> ps) -> (ps -> ps)))) -> (-. ph -> -. (((((ps -> ps) -> (-. ps -> -. ps)) -> ps) -> ps) -> ((ps -> ps) -> (ps -> ps))))) -> ph) -> ((((ps -> ps) -> (-. ps -> -. -. -. ph)) -> ps) -> ph)) -> ((((((ps -> ps) -> (-. ps -> -. -. -. ph)) -> ps) -> ph) -> ((ph -> ps) -> (-. -. ph -> ps))) -> ((((((ps -> ps) -> (-. ps -> -. ps)) -> ps) -> ps) -> ((ps -> ps) -> (ps -> ps))) -> ((ph -> ps) -> (-. -. ph -> ps)))))
7	5, 6	ax-mp 5	. . 3 |- ((((((ps -> ps) -> (-. ps -> -. -. -. ph)) -> ps) -> ph) -> ((ph -> ps) -> (-. -. ph -> ps))) -> ((((((ps -> ps) -> (-. ps -> -. ps)) -> ps) -> ps) -> ((ps -> ps) -> (ps -> ps))) -> ((ph -> ps) -> (-. -. ph -> ps))))
8	2, 7	ax-mp 5	. 2 |- ((((((ps -> ps) -> (-. ps -> -. ps)) -> ps) -> ps) -> ((ps -> ps) -> (ps -> ps))) -> ((ph -> ps) -> (-. -. ph -> ps)))
9	1, 8	ax-mp 5	1 |- ((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:  merlem12  1418  merlem13  1419  luk-2  1421