Theorem merlem7 1413

Description: Between steps 14 and 15 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.)

Assertion

Ref	Expression
merlem7	⊢ (φ → (((ψ → χ) → θ) → (((χ → τ) → (¬ θ → ¬ ψ)) → θ)))

Proof of Theorem merlem7

Step	Hyp	Ref	Expression
1		merlem4 1410	. 2 ⊢ ((ψ → χ) → (((ψ → χ) → θ) → (((χ → τ) → (¬ θ → ¬ ψ)) → θ)))
2		merlem6 1412	. . . 4 ⊢ ((((χ → τ) → (¬ θ → ¬ ψ)) → θ) → (((((ψ → χ) → θ) → (((χ → τ) → (¬ θ → ¬ ψ)) → θ)) → ¬ φ) → (¬ χ → ¬ φ)))
3		ax-meredith 1406	. . . 4 ⊢ (((((χ → τ) → (¬ θ → ¬ ψ)) → θ) → (((((ψ → χ) → θ) → (((χ → τ) → (¬ θ → ¬ ψ)) → θ)) → ¬ φ) → (¬ χ → ¬ φ))) → (((((((ψ → χ) → θ) → (((χ → τ) → (¬ θ → ¬ ψ)) → θ)) → ¬ φ) → (¬ χ → ¬ φ)) → χ) → (ψ → χ)))
4	2, 3	ax-mp 5	. . 3 ⊢ (((((((ψ → χ) → θ) → (((χ → τ) → (¬ θ → ¬ ψ)) → θ)) → ¬ φ) → (¬ χ → ¬ φ)) → χ) → (ψ → χ))
5		ax-meredith 1406	. . 3 ⊢ ((((((((ψ → χ) → θ) → (((χ → τ) → (¬ θ → ¬ ψ)) → θ)) → ¬ φ) → (¬ χ → ¬ φ)) → χ) → (ψ → χ)) → (((ψ → χ) → (((ψ → χ) → θ) → (((χ → τ) → (¬ θ → ¬ ψ)) → θ))) → (φ → (((ψ → χ) → θ) → (((χ → τ) → (¬ θ → ¬ ψ)) → θ)))))
6	4, 5	ax-mp 5	. 2 ⊢ (((ψ → χ) → (((ψ → χ) → θ) → (((χ → τ) → (¬ θ → ¬ ψ)) → θ))) → (φ → (((ψ → χ) → θ) → (((χ → τ) → (¬ θ → ¬ ψ)) → θ))))
7	1, 6	ax-mp 5	1 ⊢ (φ → (((ψ → χ) → θ) → (((χ → τ) → (¬ θ → ¬ ψ)) → θ)))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-meredith 1406

This theorem is used by:  merlem8  1414