Metamath Proof Explorer


Theorem wl-luk-ax1

Description: ax-1 proved from Lukasiewicz's axioms. (Contributed by Wolf Lammen, 17-Dec-2018) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion wl-luk-ax1
|- ( ph -> ( ps -> ph ) )

Proof

Step Hyp Ref Expression
1 ax-luk3
 |-  ( ph -> ( -. ph -> -. ps ) )
2 wl-luk-ax3
 |-  ( ( -. ph -> -. ps ) -> ( ps -> ph ) )
3 1 2 wl-luk-syl
 |-  ( ph -> ( ps -> ph ) )