Metamath Proof Explorer


Theorem wl-luk-ax3

Description: ax-3 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-ax3
|- ( ( -. ph -> -. ps ) -> ( ps -> ph ) )

Proof

Step Hyp Ref Expression
1 ax-luk3
 |-  ( ps -> ( -. ps -> ph ) )
2 ax-luk1
 |-  ( ( -. ph -> -. ps ) -> ( ( -. ps -> ph ) -> ( -. ph -> ph ) ) )
3 1 2 wl-luk-imtrid
 |-  ( ( -. ph -> -. ps ) -> ( ps -> ( -. ph -> ph ) ) )
4 ax-luk2
 |-  ( ( -. ph -> ph ) -> ph )
5 3 4 wl-luk-imtrdi
 |-  ( ( -. ph -> -. ps ) -> ( ps -> ph ) )