Theorem merlem7 651

Description: Between steps 14 and 15 of Meredith's proof of Lukasiewicz axioms from his sole axiom.

Assertion

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

Proof of Theorem merlem7

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

Syntax hints:  ¬ wn 1   → wi 2

This theorem is referenced by:  merlem8 652

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

metamath.org