Metamath Proof Explorer

Theorem merlem13

Description: Step 35 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.)

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

Proof

Step Hyp Ref Expression
1 merlem12 
 |-  ( ( ( th -> ( -. -. ch -> ch ) ) -> -. ( ( th -> ( -. -. ch -> ch ) ) -> -. -. ph ) ) -> -. ( ( th -> ( -. -. ch -> ch ) ) -> -. -. ph ) )
2 merlem12 
 |-  ( ( ( th -> ( -. -. ch -> ch ) ) -> -. -. ph ) -> -. -. ph )
3 merlem5 
 |-  ( ( ( ( th -> ( -. -. ch -> ch ) ) -> -. -. ph ) -> -. -. ph ) -> ( -. -. ( ( th -> ( -. -. ch -> ch ) ) -> -. -. ph ) -> -. -. ph ) )
4 2 3 ax-mp 
 |-  ( -. -. ( ( th -> ( -. -. ch -> ch ) ) -> -. -. ph ) -> -. -. ph )
5 merlem6 
 |-  ( ( -. -. ( ( th -> ( -. -. ch -> ch ) ) -> -. -. ph ) -> -. -. ph ) -> ( ( ( ( -. ( ( th -> ( -. -. ch -> ch ) ) -> -. -. ph ) -> ps ) -> ( -. -. ( ( th -> ( -. -. ch -> ch ) ) -> -. -. ph ) -> -. -. ph ) ) -> -. ( ( th -> ( -. -. ch -> ch ) ) -> -. -. ph ) ) -> ( ( th -> ( -. -. ch -> ch ) ) -> -. ( ( th -> ( -. -. ch -> ch ) ) -> -. -. ph ) ) ) )
6 4 5 ax-mp 
 |-  ( ( ( ( -. ( ( th -> ( -. -. ch -> ch ) ) -> -. -. ph ) -> ps ) -> ( -. -. ( ( th -> ( -. -. ch -> ch ) ) -> -. -. ph ) -> -. -. ph ) ) -> -. ( ( th -> ( -. -. ch -> ch ) ) -> -. -. ph ) ) -> ( ( th -> ( -. -. ch -> ch ) ) -> -. ( ( th -> ( -. -. ch -> ch ) ) -> -. -. ph ) ) )
7 meredith 
 |-  ( ( ( ( ( -. ( ( th -> ( -. -. ch -> ch ) ) -> -. -. ph ) -> ps ) -> ( -. -. ( ( th -> ( -. -. ch -> ch ) ) -> -. -. ph ) -> -. -. ph ) ) -> -. ( ( th -> ( -. -. ch -> ch ) ) -> -. -. ph ) ) -> ( ( th -> ( -. -. ch -> ch ) ) -> -. ( ( th -> ( -. -. ch -> ch ) ) -> -. -. ph ) ) ) -> ( ( ( ( th -> ( -. -. ch -> ch ) ) -> -. ( ( th -> ( -. -. ch -> ch ) ) -> -. -. ph ) ) -> -. ( ( th -> ( -. -. ch -> ch ) ) -> -. -. ph ) ) -> ( -. ph -> -. ( ( th -> ( -. -. ch -> ch ) ) -> -. -. ph ) ) ) )
8 6 7 ax-mp 
 |-  ( ( ( ( th -> ( -. -. ch -> ch ) ) -> -. ( ( th -> ( -. -. ch -> ch ) ) -> -. -. ph ) ) -> -. ( ( th -> ( -. -. ch -> ch ) ) -> -. -. ph ) ) -> ( -. ph -> -. ( ( th -> ( -. -. ch -> ch ) ) -> -. -. ph ) ) )
9 1 8 ax-mp 
 |-  ( -. ph -> -. ( ( th -> ( -. -. ch -> ch ) ) -> -. -. ph ) )
10 merlem6 
 |-  ( ( -. ph -> -. ( ( th -> ( -. -. ch -> ch ) ) -> -. -. ph ) ) -> ( ( ( ( ps -> ps ) -> ( -. ph -> -. ( ( th -> ( -. -. ch -> ch ) ) -> -. -. ph ) ) ) -> ph ) -> ( ( ( ( ps -> ps ) -> ( -. ph -> -. ( ( th -> ( -. -. ch -> ch ) ) -> -. -. ph ) ) ) -> ph ) -> ph ) ) )
11 9 10 ax-mp 
 |-  ( ( ( ( ps -> ps ) -> ( -. ph -> -. ( ( th -> ( -. -. ch -> ch ) ) -> -. -. ph ) ) ) -> ph ) -> ( ( ( ( ps -> ps ) -> ( -. ph -> -. ( ( th -> ( -. -. ch -> ch ) ) -> -. -. ph ) ) ) -> ph ) -> ph ) )
12 merlem11 
 |-  ( ( ( ( ( ps -> ps ) -> ( -. ph -> -. ( ( th -> ( -. -. ch -> ch ) ) -> -. -. ph ) ) ) -> ph ) -> ( ( ( ( ps -> ps ) -> ( -. ph -> -. ( ( th -> ( -. -. ch -> ch ) ) -> -. -. ph ) ) ) -> ph ) -> ph ) ) -> ( ( ( ( ps -> ps ) -> ( -. ph -> -. ( ( th -> ( -. -. ch -> ch ) ) -> -. -. ph ) ) ) -> ph ) -> ph ) )
13 11 12 ax-mp 
 |-  ( ( ( ( ps -> ps ) -> ( -. ph -> -. ( ( th -> ( -. -. ch -> ch ) ) -> -. -. ph ) ) ) -> ph ) -> ph )
14 meredith 
 |-  ( ( ( ( ( ps -> ps ) -> ( -. ph -> -. ( ( th -> ( -. -. ch -> ch ) ) -> -. -. ph ) ) ) -> ph ) -> ph ) -> ( ( ph -> ps ) -> ( ( ( th -> ( -. -. ch -> ch ) ) -> -. -. ph ) -> ps ) ) )
15 13 14 ax-mp 
 |-  ( ( ph -> ps ) -> ( ( ( th -> ( -. -. ch -> ch ) ) -> -. -. ph ) -> ps ) )