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	$⊢ (((\neg φ \to φ) \to φ) \to ψ) \to ψ$

Proof

Step	Hyp	Ref	Expression
1		luk-2	$⊢ (\neg ((\neg φ \to φ) \to φ) \to ((\neg φ \to φ) \to φ)) \to ((\neg φ \to φ) \to φ)$
2		luk-2	$⊢ (\neg φ \to φ) \to φ$
3		luklem3	$⊢ ((\neg φ \to φ) \to φ) \to (((\neg ((\neg φ \to φ) \to φ) \to ((\neg φ \to φ) \to φ)) \to ((\neg φ \to φ) \to φ)) \to (\neg ψ \to ((\neg φ \to φ) \to φ)))$
4	2 3	ax-mp	$⊢ ((\neg ((\neg φ \to φ) \to φ) \to ((\neg φ \to φ) \to φ)) \to ((\neg φ \to φ) \to φ)) \to (\neg ψ \to ((\neg φ \to φ) \to φ))$
5	1 4	ax-mp	$⊢ \neg ψ \to ((\neg φ \to φ) \to φ)$
6		luk-1	$⊢ (\neg ψ \to ((\neg φ \to φ) \to φ)) \to ((((\neg φ \to φ) \to φ) \to ψ) \to (\neg ψ \to ψ))$
7	5 6	ax-mp	$⊢ (((\neg φ \to φ) \to φ) \to ψ) \to (\neg ψ \to ψ)$
8		luk-2	$⊢ (\neg ψ \to ψ) \to ψ$
9	7 8	luklem1	$⊢ (((\neg φ \to φ) \to φ) \to ψ) \to ψ$