Theorem merlem1 645

Description: Step 3 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (The step numbers refer to Meredith's original paper.)

Assertion

Ref	Expression
merlem1	⊢ (((χ → (¬ φ → ψ)) → τ) → (φ → τ))

Proof of Theorem merlem1

Step	Hyp	Ref	Expression
1		meredith 644	. . 3 ⊢ (((((¬ φ → ψ) → (¬ (¬ τ → ¬ χ) → ¬ ¬ (¬ φ → ψ))) → (¬ τ → ¬ χ)) → τ) → ((τ → ¬ φ) → (¬ (¬ φ → ψ) → ¬ φ)))
2		meredith 644	. . 3 ⊢ ((((((¬ φ → ψ) → (¬ (¬ τ → ¬ χ) → ¬ ¬ (¬ φ → ψ))) → (¬ τ → ¬ χ)) → τ) → ((τ → ¬ φ) → (¬ (¬ φ → ψ) → ¬ φ))) → ((((τ → ¬ φ) → (¬ (¬ φ → ψ) → ¬ φ)) → (¬ φ → ψ)) → (χ → (¬ φ → ψ))))
3	1, 2	ax-mp 6	. 2 ⊢ ((((τ → ¬ φ) → (¬ (¬ φ → ψ) → ¬ φ)) → (¬ φ → ψ)) → (χ → (¬ φ → ψ)))
4		meredith 644	. 2 ⊢ (((((τ → ¬ φ) → (¬ (¬ φ → ψ) → ¬ φ)) → (¬ φ → ψ)) → (χ → (¬ φ → ψ))) → (((χ → (¬ φ → ψ)) → τ) → (φ → τ)))
5	3, 4	ax-mp 6	1 ⊢ (((χ → (¬ φ → ψ)) → τ) → (φ → τ))

Syntax hints:  ¬ wn 1   → wi 2

This theorem is referenced by:  merlem2 646  merlem5 649  luk-3 660

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

metamath.org