Metamath Proof Explorer

Theorem merlem9

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

		Ref	Expression
	Assertion	merlem9	$⊢ ((φ \to ψ) \to (χ \to (θ \to (ψ \to τ)))) \to (η \to (χ \to (θ \to (ψ \to τ))))$

Proof

Step	Hyp	Ref	Expression
1		merlem6	$⊢ (θ \to (ψ \to τ)) \to (((χ \to (θ \to (ψ \to τ))) \to \neg η) \to (\neg ψ \to \neg η))$
2		merlem8	$⊢ ((θ \to (ψ \to τ)) \to (((χ \to (θ \to (ψ \to τ))) \to \neg η) \to (\neg ψ \to \neg η))) \to ((((ψ \to τ) \to (\neg (\neg (((χ \to (θ \to (ψ \to τ))) \to \neg η) \to (\neg ψ \to \neg η)) \to \neg θ) \to \neg φ)) \to (\neg (((χ \to (θ \to (ψ \to τ))) \to \neg η) \to (\neg ψ \to \neg η)) \to \neg θ)) \to (((χ \to (θ \to (ψ \to τ))) \to \neg η) \to (\neg ψ \to \neg η)))$
3	1 2	ax-mp	$⊢ (((ψ \to τ) \to (\neg (\neg (((χ \to (θ \to (ψ \to τ))) \to \neg η) \to (\neg ψ \to \neg η)) \to \neg θ) \to \neg φ)) \to (\neg (((χ \to (θ \to (ψ \to τ))) \to \neg η) \to (\neg ψ \to \neg η)) \to \neg θ)) \to (((χ \to (θ \to (ψ \to τ))) \to \neg η) \to (\neg ψ \to \neg η))$
4		meredith	$⊢ ((((ψ \to τ) \to (\neg (\neg (((χ \to (θ \to (ψ \to τ))) \to \neg η) \to (\neg ψ \to \neg η)) \to \neg θ) \to \neg φ)) \to (\neg (((χ \to (θ \to (ψ \to τ))) \to \neg η) \to (\neg ψ \to \neg η)) \to \neg θ)) \to (((χ \to (θ \to (ψ \to τ))) \to \neg η) \to (\neg ψ \to \neg η))) \to (((((χ \to (θ \to (ψ \to τ))) \to \neg η) \to (\neg ψ \to \neg η)) \to ψ) \to (φ \to ψ))$
5	3 4	ax-mp	$⊢ ((((χ \to (θ \to (ψ \to τ))) \to \neg η) \to (\neg ψ \to \neg η)) \to ψ) \to (φ \to ψ)$
6		meredith	$⊢ (((((χ \to (θ \to (ψ \to τ))) \to \neg η) \to (\neg ψ \to \neg η)) \to ψ) \to (φ \to ψ)) \to (((φ \to ψ) \to (χ \to (θ \to (ψ \to τ)))) \to (η \to (χ \to (θ \to (ψ \to τ)))))$
7	5 6	ax-mp	$⊢ ((φ \to ψ) \to (χ \to (θ \to (ψ \to τ)))) \to (η \to (χ \to (θ \to (ψ \to τ))))$