Metamath Proof Explorer

Theorem merlem1

Description: Step 3 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (The step numbers refer to Meredith's original paper.) (Contributed by NM, 14-Dec-2002) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	merlem1	$⊢ ((χ \to (\neg φ \to ψ)) \to τ) \to (φ \to τ)$

Proof

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