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 ¬ φ ¬ ψ ψ φ