Metamath Proof Explorer

Theorem luklem4

Description: Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion luklem4 
|- ( ( ( ( -. ph -> ph ) -> ph ) -> ps ) -> ps )

Proof

Step Hyp Ref Expression
1 luk-2 
 |-  ( ( -. ( ( -. ph -> ph ) -> ph ) -> ( ( -. ph -> ph ) -> ph ) ) -> ( ( -. ph -> ph ) -> ph ) )
2 luk-2 
 |-  ( ( -. ph -> ph ) -> ph )
3 luklem3 
 |-  ( ( ( -. ph -> ph ) -> ph ) -> ( ( ( -. ( ( -. ph -> ph ) -> ph ) -> ( ( -. ph -> ph ) -> ph ) ) -> ( ( -. ph -> ph ) -> ph ) ) -> ( -. ps -> ( ( -. ph -> ph ) -> ph ) ) ) )
4 2 3 ax-mp 
 |-  ( ( ( -. ( ( -. ph -> ph ) -> ph ) -> ( ( -. ph -> ph ) -> ph ) ) -> ( ( -. ph -> ph ) -> ph ) ) -> ( -. ps -> ( ( -. ph -> ph ) -> ph ) ) )
5 1 4 ax-mp 
 |-  ( -. ps -> ( ( -. ph -> ph ) -> ph ) )
6 luk-1 
 |-  ( ( -. ps -> ( ( -. ph -> ph ) -> ph ) ) -> ( ( ( ( -. ph -> ph ) -> ph ) -> ps ) -> ( -. ps -> ps ) ) )
7 5 6 ax-mp 
 |-  ( ( ( ( -. ph -> ph ) -> ph ) -> ps ) -> ( -. ps -> ps ) )
8 luk-2 
 |-  ( ( -. ps -> ps ) -> ps )
9 7 8 luklem1 
 |-  ( ( ( ( -. ph -> ph ) -> ph ) -> ps ) -> ps )