This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem merlem7

Description: Between steps 14 and 15 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.)

Ref Expression
Assertion merlem7 
|- ( ph -> ( ( ( ps -> ch ) -> th ) -> ( ( ( ch -> ta ) -> ( -. th -> -. ps ) ) -> th ) ) )

Proof

Step Hyp Ref Expression
1 merlem4 
 |-  ( ( ps -> ch ) -> ( ( ( ps -> ch ) -> th ) -> ( ( ( ch -> ta ) -> ( -. th -> -. ps ) ) -> th ) ) )
2 merlem6 
 |-  ( ( ( ( ch -> ta ) -> ( -. th -> -. ps ) ) -> th ) -> ( ( ( ( ( ps -> ch ) -> th ) -> ( ( ( ch -> ta ) -> ( -. th -> -. ps ) ) -> th ) ) -> -. ph ) -> ( -. ch -> -. ph ) ) )
3 meredith 
 |-  ( ( ( ( ( ch -> ta ) -> ( -. th -> -. ps ) ) -> th ) -> ( ( ( ( ( ps -> ch ) -> th ) -> ( ( ( ch -> ta ) -> ( -. th -> -. ps ) ) -> th ) ) -> -. ph ) -> ( -. ch -> -. ph ) ) ) -> ( ( ( ( ( ( ( ps -> ch ) -> th ) -> ( ( ( ch -> ta ) -> ( -. th -> -. ps ) ) -> th ) ) -> -. ph ) -> ( -. ch -> -. ph ) ) -> ch ) -> ( ps -> ch ) ) )
4 2 3 ax-mp 
 |-  ( ( ( ( ( ( ( ps -> ch ) -> th ) -> ( ( ( ch -> ta ) -> ( -. th -> -. ps ) ) -> th ) ) -> -. ph ) -> ( -. ch -> -. ph ) ) -> ch ) -> ( ps -> ch ) )
5 meredith 
 |-  ( ( ( ( ( ( ( ( ps -> ch ) -> th ) -> ( ( ( ch -> ta ) -> ( -. th -> -. ps ) ) -> th ) ) -> -. ph ) -> ( -. ch -> -. ph ) ) -> ch ) -> ( ps -> ch ) ) -> ( ( ( ps -> ch ) -> ( ( ( ps -> ch ) -> th ) -> ( ( ( ch -> ta ) -> ( -. th -> -. ps ) ) -> th ) ) ) -> ( ph -> ( ( ( ps -> ch ) -> th ) -> ( ( ( ch -> ta ) -> ( -. th -> -. ps ) ) -> th ) ) ) ) )
6 4 5 ax-mp 
 |-  ( ( ( ps -> ch ) -> ( ( ( ps -> ch ) -> th ) -> ( ( ( ch -> ta ) -> ( -. th -> -. ps ) ) -> th ) ) ) -> ( ph -> ( ( ( ps -> ch ) -> th ) -> ( ( ( ch -> ta ) -> ( -. th -> -. ps ) ) -> th ) ) ) )
7 1 6 ax-mp 
 |-  ( ph -> ( ( ( ps -> ch ) -> th ) -> ( ( ( ch -> ta ) -> ( -. th -> -. ps ) ) -> th ) ) )