Theorem merlem9 1415

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

Assertion

Ref	Expression
merlem9	|- (((ph -> ps) -> (ch -> (th -> (ps -> ta)))) -> (et -> (ch -> (th -> (ps -> ta)))))

Proof of Theorem merlem9

Step	Hyp	Ref	Expression
1		merlem6 1412	. . . 4 |- ((th -> (ps -> ta)) -> (((ch -> (th -> (ps -> ta))) -> -. et) -> (-. ps -> -. et)))
2		merlem8 1414	. . . 4 |- (((th -> (ps -> ta)) -> (((ch -> (th -> (ps -> ta))) -> -. et) -> (-. ps -> -. et))) -> ((((ps -> ta) -> (-. (-. (((ch -> (th -> (ps -> ta))) -> -. et) -> (-. ps -> -. et)) -> -. th) -> -. ph)) -> (-. (((ch -> (th -> (ps -> ta))) -> -. et) -> (-. ps -> -. et)) -> -. th)) -> (((ch -> (th -> (ps -> ta))) -> -. et) -> (-. ps -> -. et))))
3	1, 2	ax-mp 5	. . 3 |- ((((ps -> ta) -> (-. (-. (((ch -> (th -> (ps -> ta))) -> -. et) -> (-. ps -> -. et)) -> -. th) -> -. ph)) -> (-. (((ch -> (th -> (ps -> ta))) -> -. et) -> (-. ps -> -. et)) -> -. th)) -> (((ch -> (th -> (ps -> ta))) -> -. et) -> (-. ps -> -. et)))
4		ax-meredith 1406	. . 3 |- (((((ps -> ta) -> (-. (-. (((ch -> (th -> (ps -> ta))) -> -. et) -> (-. ps -> -. et)) -> -. th) -> -. ph)) -> (-. (((ch -> (th -> (ps -> ta))) -> -. et) -> (-. ps -> -. et)) -> -. th)) -> (((ch -> (th -> (ps -> ta))) -> -. et) -> (-. ps -> -. et))) -> (((((ch -> (th -> (ps -> ta))) -> -. et) -> (-. ps -> -. et)) -> ps) -> (ph -> ps)))
5	3, 4	ax-mp 5	. 2 |- (((((ch -> (th -> (ps -> ta))) -> -. et) -> (-. ps -> -. et)) -> ps) -> (ph -> ps))
6		ax-meredith 1406	. 2 |- ((((((ch -> (th -> (ps -> ta))) -> -. et) -> (-. ps -> -. et)) -> ps) -> (ph -> ps)) -> (((ph -> ps) -> (ch -> (th -> (ps -> ta)))) -> (et -> (ch -> (th -> (ps -> ta))))))
7	5, 6	ax-mp 5	1 |- (((ph -> ps) -> (ch -> (th -> (ps -> ta)))) -> (et -> (ch -> (th -> (ps -> ta)))))

Syntax hints:  -. wn 3   -> wi 4

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

This theorem is referenced by:  merlem10  1416