Metamath Proof Explorer


Theorem luklem3

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 luklem3 φ¬φψχθχ

Proof

Step Hyp Ref Expression
1 luk-3 φ¬φ¬θ
2 luklem2 ¬φ¬θ¬φψχθχ
3 1 2 luklem1 φ¬φψχθχ