Theorem merlem1 1407

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.)

Assertion

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

Proof of Theorem merlem1

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

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-meredith 1406

This theorem is referenced by:  merlem2  1408  merlem5  1411  luk-3  1422