Metamath Proof Explorer


Theorem luklem4

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

Proof

Step Hyp Ref Expression
1 luk-2 ¬ ¬ φ φ φ ¬ φ φ φ ¬ φ φ φ
2 luk-2 ¬ φ φ φ
3 luklem3 ¬ φ φ φ ¬ ¬ φ φ φ ¬ φ φ φ ¬ φ φ φ ¬ ψ ¬ φ φ φ
4 2 3 ax-mp ¬ ¬ φ φ φ ¬ φ φ φ ¬ φ φ φ ¬ ψ ¬ φ φ φ
5 1 4 ax-mp ¬ ψ ¬ φ φ φ
6 luk-1 ¬ ψ ¬ φ φ φ ¬ φ φ φ ψ ¬ ψ ψ
7 5 6 ax-mp ¬ φ φ φ ψ ¬ ψ ψ
8 luk-2 ¬ ψ ψ ψ
9 7 8 luklem1 ¬ φ φ φ ψ ψ