Metamath Proof Explorer


Theorem luklem3

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 luklem3
|- ( ph -> ( ( ( -. ph -> ps ) -> ch ) -> ( th -> ch ) ) )

Proof

Step Hyp Ref Expression
1 luk-3
 |-  ( ph -> ( -. ph -> -. th ) )
2 luklem2
 |-  ( ( -. ph -> -. th ) -> ( ( ( -. ph -> ps ) -> ch ) -> ( th -> ch ) ) )
3 1 2 luklem1
 |-  ( ph -> ( ( ( -. ph -> ps ) -> ch ) -> ( th -> ch ) ) )