Metamath Proof Explorer


Theorem luklem8

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 luklem8 ( ( 𝜑𝜓 ) → ( ( 𝜒𝜑 ) → ( 𝜒𝜓 ) ) )

Proof

Step Hyp Ref Expression
1 luk-1 ( ( 𝜒𝜑 ) → ( ( 𝜑𝜓 ) → ( 𝜒𝜓 ) ) )
2 luklem7 ( ( ( 𝜒𝜑 ) → ( ( 𝜑𝜓 ) → ( 𝜒𝜓 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜒𝜑 ) → ( 𝜒𝜓 ) ) ) )
3 1 2 ax-mp ( ( 𝜑𝜓 ) → ( ( 𝜒𝜑 ) → ( 𝜒𝜓 ) ) )