Theorem merlem9 653

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 650	. . . 4 |- ((th -> (ps -> ta )) -> (((ch -> (th -> (ps -> ta ))) -> -. et) -> (-. ps -> -. et)))
2		merlem8 652	. . . 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 6	. . 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 644	. . 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 6	. 2 |- (((((ch -> (th -> (ps -> ta ))) -> -. et) -> (-. ps -> -. et)) -> ps) -> (ph -> ps))
6		meredith 644	. 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 6	1 |- (((ph -> ps) -> (ch -> (th -> (ps -> ta )))) -> (et -> (ch -> (th -> (ps -> ta )))))

Syntax hints:  -. wn 1   -> wi 2

This theorem is referenced by:  merlem10 654

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

metamath.org