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

Proof

Step Hyp Ref Expression
1 luklem2 ( ( ¬ 𝜑 → ¬ 𝜓 ) → ( ( ( ¬ 𝜑𝜑 ) → 𝜑 ) → ( 𝜓𝜑 ) ) )
2 luklem4 ( ( ( ( ¬ 𝜑𝜑 ) → 𝜑 ) → ( 𝜓𝜑 ) ) → ( 𝜓𝜑 ) )
3 1 2 luklem1 ( ( ¬ 𝜑 → ¬ 𝜓 ) → ( 𝜓𝜑 ) )