Theorem merlem13 1419

Description: Step 35 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (Contributed by NM, 14-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

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

Proof of Theorem merlem13

Step	Hyp	Ref	Expression
1		merlem12 1418	. . . . 5 ⊢ (((θ → (¬ ¬ χ → χ)) → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ)) → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ))
2		merlem12 1418	. . . . . . . 8 ⊢ (((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ) → ¬ ¬ φ)
3		merlem5 1411	. . . . . . . 8 ⊢ ((((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ) → ¬ ¬ φ) → (¬ ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ) → ¬ ¬ φ))
4	2, 3	ax-mp 5	. . . . . . 7 ⊢ (¬ ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ) → ¬ ¬ φ)
5		merlem6 1412	. . . . . . 7 ⊢ ((¬ ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ) → ¬ ¬ φ) → ((((¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ) → ψ) → (¬ ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ) → ¬ ¬ φ)) → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ)) → ((θ → (¬ ¬ χ → χ)) → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ))))
6	4, 5	ax-mp 5	. . . . . 6 ⊢ ((((¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ) → ψ) → (¬ ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ) → ¬ ¬ φ)) → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ)) → ((θ → (¬ ¬ χ → χ)) → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ)))
7		ax-meredith 1406	. . . . . 6 ⊢ (((((¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ) → ψ) → (¬ ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ) → ¬ ¬ φ)) → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ)) → ((θ → (¬ ¬ χ → χ)) → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ))) → ((((θ → (¬ ¬ χ → χ)) → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ)) → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ)) → (¬ φ → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ))))
8	6, 7	ax-mp 5	. . . . 5 ⊢ ((((θ → (¬ ¬ χ → χ)) → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ)) → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ)) → (¬ φ → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ)))
9	1, 8	ax-mp 5	. . . 4 ⊢ (¬ φ → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ))
10		merlem6 1412	. . . 4 ⊢ ((¬ φ → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ)) → ((((ψ → ψ) → (¬ φ → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ))) → φ) → ((((ψ → ψ) → (¬ φ → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ))) → φ) → φ)))
11	9, 10	ax-mp 5	. . 3 ⊢ ((((ψ → ψ) → (¬ φ → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ))) → φ) → ((((ψ → ψ) → (¬ φ → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ))) → φ) → φ))
12		merlem11 1417	. . 3 ⊢ (((((ψ → ψ) → (¬ φ → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ))) → φ) → ((((ψ → ψ) → (¬ φ → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ))) → φ) → φ)) → ((((ψ → ψ) → (¬ φ → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ))) → φ) → φ))
13	11, 12	ax-mp 5	. 2 ⊢ ((((ψ → ψ) → (¬ φ → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ))) → φ) → φ)
14		ax-meredith 1406	. 2 ⊢ (((((ψ → ψ) → (¬ φ → ¬ ((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ))) → φ) → φ) → ((φ → ψ) → (((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ) → ψ)))
15	13, 14	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:  luk-1  1420