Metamath Proof Explorer

Theorem luklem6

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

Proof

Step	Hyp	Ref	Expression
1		luk-1	$⊢ (φ \to (φ \to ψ)) \to (((φ \to ψ) \to ψ) \to (φ \to ψ))$
2		luklem5	$⊢ \neg (φ \to ψ) \to (\neg ψ \to \neg (φ \to ψ))$
3		luklem2	$⊢ (\neg ψ \to \neg (φ \to ψ)) \to (((\neg ψ \to ψ) \to ψ) \to ((φ \to ψ) \to ψ))$
4		luklem4	$⊢ (((\neg ψ \to ψ) \to ψ) \to ((φ \to ψ) \to ψ)) \to ((φ \to ψ) \to ψ)$
5	3 4	luklem1	$⊢ (\neg ψ \to \neg (φ \to ψ)) \to ((φ \to ψ) \to ψ)$
6	2 5	luklem1	$⊢ \neg (φ \to ψ) \to ((φ \to ψ) \to ψ)$
7		luk-1	$⊢ (\neg (φ \to ψ) \to ((φ \to ψ) \to ψ)) \to ((((φ \to ψ) \to ψ) \to (φ \to ψ)) \to (\neg (φ \to ψ) \to (φ \to ψ)))$
8	6 7	ax-mp	$⊢ (((φ \to ψ) \to ψ) \to (φ \to ψ)) \to (\neg (φ \to ψ) \to (φ \to ψ))$
9		luk-1	$⊢ ((((φ \to ψ) \to ψ) \to (φ \to ψ)) \to (\neg (φ \to ψ) \to (φ \to ψ))) \to (((\neg (φ \to ψ) \to (φ \to ψ)) \to (φ \to ψ)) \to ((((φ \to ψ) \to ψ) \to (φ \to ψ)) \to (φ \to ψ)))$
10	8 9	ax-mp	$⊢ ((\neg (φ \to ψ) \to (φ \to ψ)) \to (φ \to ψ)) \to ((((φ \to ψ) \to ψ) \to (φ \to ψ)) \to (φ \to ψ))$
11		luklem4	$⊢ (((\neg (φ \to ψ) \to (φ \to ψ)) \to (φ \to ψ)) \to ((((φ \to ψ) \to ψ) \to (φ \to ψ)) \to (φ \to ψ))) \to ((((φ \to ψ) \to ψ) \to (φ \to ψ)) \to (φ \to ψ))$
12	10 11	ax-mp	$⊢ (((φ \to ψ) \to ψ) \to (φ \to ψ)) \to (φ \to ψ)$
13	1 12	luklem1	$⊢ (φ \to (φ \to ψ)) \to (φ \to ψ)$