Theorem merlem13 657

Description: Step 35 of Meredith's proof of Lukasiewicz axioms from his sole axiom.

Assertion

Ref	Expression
merlem13	⊢ ((φ → ψ) → (((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ) → ψ))

Proof of Theorem merlem13

Step	Hyp	Ref	Expression
1		merlem12 656	. . . . 5 ⊢ (((θ → (¬ ¬ χ → χ)) → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ)) → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ))
2		merlem12 656	. . . . . . . 8 ⊢ (((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ) → ¬ ¬ φ)
3		merlem5 649	. . . . . . . 8 ⊢ ((((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ) → ¬ ¬ φ) → (¬ ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ) → ¬ ¬ φ))
4	2, 3	ax-mp 6	. . . . . . 7 ⊢ (¬ ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ) → ¬ ¬ φ)
5		merlem6 650	. . . . . . 7 ⊢ ((¬ ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ) → ¬ ¬ φ) → ((((¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ) → ψ) → (¬ ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ) → ¬ ¬ φ)) → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ)) → ((θ → (¬ ¬ χ → χ)) → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ))))
6	4, 5	ax-mp 6	. . . . . 6 ⊢ ((((¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ) → ψ) → (¬ ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ) → ¬ ¬ φ)) → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ)) → ((θ → (¬ ¬ χ → χ)) → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ)))
7		meredith 644	. . . . . 6 ⊢ (((((¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ) → ψ) → (¬ ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ) → ¬ ¬ φ)) → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ)) → ((θ → (¬ ¬ χ → χ)) → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ))) → ((((θ → (¬ ¬ χ → χ)) → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ)) → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ)) → (¬ φ → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ))))
8	6, 7	ax-mp 6	. . . . 5 ⊢ ((((θ → (¬ ¬ χ → χ)) → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ)) → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ)) → (¬ φ → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ)))
9	1, 8	ax-mp 6	. . . 4 ⊢ (¬ φ → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ))
10		merlem6 650	. . . 4 ⊢ ((¬ φ → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ)) → ((((ψ → ψ) → (¬ φ → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ))) → φ) → ((((ψ → ψ) → (¬ φ → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ))) → φ) → φ)))
11	9, 10	ax-mp 6	. . 3 ⊢ ((((ψ → ψ) → (¬ φ → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ))) → φ) → ((((ψ → ψ) → (¬ φ → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ))) → φ) → φ))
12		merlem11 655	. . 3 ⊢ (((((ψ → ψ) → (¬ φ → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ))) → φ) → ((((ψ → ψ) → (¬ φ → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ))) → φ) → φ)) → ((((ψ → ψ) → (¬ φ → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ))) → φ) → φ))
13	11, 12	ax-mp 6	. 2 ⊢ ((((ψ → ψ) → (¬ φ → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ))) → φ) → φ)
14		meredith 644	. 2 ⊢ (((((ψ → ψ) → (¬ φ → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ))) → φ) → φ) → ((φ → ψ) → (((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ) → ψ)))
15	13, 14	ax-mp 6	1 ⊢ ((φ → ψ) → (((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ) → ψ))

Syntax hints:  ¬ wn 1   → wi 2

This theorem is referenced by:  luk-1 658

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

metamath.org