Theorem merlem9 933

Description: Step 18 of Meredith's proof of Lukasiewicz axioms from his sole axiom.

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 930	. . . 4 |- ((th -> (ps -> ta)) -> (((ch -> (th -> (ps -> ta))) -> -. et) -> (-. ps -> -. et)))
2		merlem8 932	. . . 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 7	. . 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		meredith 924	. . 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 7	. 2 |- (((((ch -> (th -> (ps -> ta))) -> -. et) -> (-. ps -> -. et)) -> ps) -> (ph -> ps))
6		meredith 924	. 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 7	1 |- (((ph -> ps) -> (ch -> (th -> (ps -> ta)))) -> (et -> (ch -> (th -> (ps -> ta)))))

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  merlem10 934

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

Copyright terms: Public domain