Metamath Proof Explorer


Theorem luklem5

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 luklem5
|- ( ph -> ( ps -> ph ) )

Proof

Step Hyp Ref Expression
1 luklem3
 |-  ( ph -> ( ( ( -. ph -> ph ) -> ph ) -> ( ps -> ph ) ) )
2 luklem4
 |-  ( ( ( ( -. ph -> ph ) -> ph ) -> ( ps -> ph ) ) -> ( ps -> ph ) )
3 1 2 luklem1
 |-  ( ph -> ( ps -> ph ) )