Metamath Proof Explorer

Theorem merlem13

Description: Step 35 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (Contributed by NM, 14-Dec-2002) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	merlem13	$⊢ (φ \to ψ) \to (((θ \to (\neg \neg χ \to χ)) \to \neg \neg φ) \to ψ)$

Proof

Step	Hyp	Ref	Expression
1		merlem12	$⊢ ((θ \to (\neg \neg χ \to χ)) \to \neg ((θ \to (\neg \neg χ \to χ)) \to \neg \neg φ)) \to \neg ((θ \to (\neg \neg χ \to χ)) \to \neg \neg φ)$
2		merlem12	$⊢ ((θ \to (\neg \neg χ \to χ)) \to \neg \neg φ) \to \neg \neg φ$
3		merlem5	$⊢ (((θ \to (\neg \neg χ \to χ)) \to \neg \neg φ) \to \neg \neg φ) \to (\neg \neg ((θ \to (\neg \neg χ \to χ)) \to \neg \neg φ) \to \neg \neg φ)$
4	2 3	ax-mp	$⊢ \neg \neg ((θ \to (\neg \neg χ \to χ)) \to \neg \neg φ) \to \neg \neg φ$
5		merlem6	$⊢ (\neg \neg ((θ \to (\neg \neg χ \to χ)) \to \neg \neg φ) \to \neg \neg φ) \to ((((\neg ((θ \to (\neg \neg χ \to χ)) \to \neg \neg φ) \to ψ) \to (\neg \neg ((θ \to (\neg \neg χ \to χ)) \to \neg \neg φ) \to \neg \neg φ)) \to \neg ((θ \to (\neg \neg χ \to χ)) \to \neg \neg φ)) \to ((θ \to (\neg \neg χ \to χ)) \to \neg ((θ \to (\neg \neg χ \to χ)) \to \neg \neg φ)))$
6	4 5	ax-mp	$⊢ (((\neg ((θ \to (\neg \neg χ \to χ)) \to \neg \neg φ) \to ψ) \to (\neg \neg ((θ \to (\neg \neg χ \to χ)) \to \neg \neg φ) \to \neg \neg φ)) \to \neg ((θ \to (\neg \neg χ \to χ)) \to \neg \neg φ)) \to ((θ \to (\neg \neg χ \to χ)) \to \neg ((θ \to (\neg \neg χ \to χ)) \to \neg \neg φ))$
7		meredith	$⊢ ((((\neg ((θ \to (\neg \neg χ \to χ)) \to \neg \neg φ) \to ψ) \to (\neg \neg ((θ \to (\neg \neg χ \to χ)) \to \neg \neg φ) \to \neg \neg φ)) \to \neg ((θ \to (\neg \neg χ \to χ)) \to \neg \neg φ)) \to ((θ \to (\neg \neg χ \to χ)) \to \neg ((θ \to (\neg \neg χ \to χ)) \to \neg \neg φ))) \to ((((θ \to (\neg \neg χ \to χ)) \to \neg ((θ \to (\neg \neg χ \to χ)) \to \neg \neg φ)) \to \neg ((θ \to (\neg \neg χ \to χ)) \to \neg \neg φ)) \to (\neg φ \to \neg ((θ \to (\neg \neg χ \to χ)) \to \neg \neg φ)))$
8	6 7	ax-mp	$⊢ (((θ \to (\neg \neg χ \to χ)) \to \neg ((θ \to (\neg \neg χ \to χ)) \to \neg \neg φ)) \to \neg ((θ \to (\neg \neg χ \to χ)) \to \neg \neg φ)) \to (\neg φ \to \neg ((θ \to (\neg \neg χ \to χ)) \to \neg \neg φ))$
9	1 8	ax-mp	$⊢ \neg φ \to \neg ((θ \to (\neg \neg χ \to χ)) \to \neg \neg φ)$
10		merlem6	$⊢ (\neg φ \to \neg ((θ \to (\neg \neg χ \to χ)) \to \neg \neg φ)) \to ((((ψ \to ψ) \to (\neg φ \to \neg ((θ \to (\neg \neg χ \to χ)) \to \neg \neg φ))) \to φ) \to ((((ψ \to ψ) \to (\neg φ \to \neg ((θ \to (\neg \neg χ \to χ)) \to \neg \neg φ))) \to φ) \to φ))$
11	9 10	ax-mp	$⊢ (((ψ \to ψ) \to (\neg φ \to \neg ((θ \to (\neg \neg χ \to χ)) \to \neg \neg φ))) \to φ) \to ((((ψ \to ψ) \to (\neg φ \to \neg ((θ \to (\neg \neg χ \to χ)) \to \neg \neg φ))) \to φ) \to φ)$
12		merlem11	$⊢ ((((ψ \to ψ) \to (\neg φ \to \neg ((θ \to (\neg \neg χ \to χ)) \to \neg \neg φ))) \to φ) \to ((((ψ \to ψ) \to (\neg φ \to \neg ((θ \to (\neg \neg χ \to χ)) \to \neg \neg φ))) \to φ) \to φ)) \to ((((ψ \to ψ) \to (\neg φ \to \neg ((θ \to (\neg \neg χ \to χ)) \to \neg \neg φ))) \to φ) \to φ)$
13	11 12	ax-mp	$⊢ (((ψ \to ψ) \to (\neg φ \to \neg ((θ \to (\neg \neg χ \to χ)) \to \neg \neg φ))) \to φ) \to φ$
14		meredith	$⊢ ((((ψ \to ψ) \to (\neg φ \to \neg ((θ \to (\neg \neg χ \to χ)) \to \neg \neg φ))) \to φ) \to φ) \to ((φ \to ψ) \to (((θ \to (\neg \neg χ \to χ)) \to \neg \neg φ) \to ψ))$
15	13 14	ax-mp	$⊢ (φ \to ψ) \to (((θ \to (\neg \neg χ \to χ)) \to \neg \neg φ) \to ψ)$