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