Metamath Proof Explorer


Theorem ax3

Description: Standard propositional axiom derived from Lukasiewicz axioms. (Contributed by NM, 22-Dec-2002) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

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