Theorem luk-1 1687

Description: 1 of 3 axioms for propositional calculus due to Lukasiewicz, derived from Meredith's sole axiom. (Contributed by NM, 14-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
luk-1	⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒)))

Proof of Theorem luk-1

Step	Hyp	Ref	Expression
1		meredith 1673	. 2 ⊢ (((((𝜒 → 𝜒) → (¬ ¬ ¬ 𝜑 → ¬ 𝜑)) → ¬ ¬ 𝜑) → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒)))
2		merlem13 1686	. . . 4 ⊢ ((𝜑 → 𝜓) → ((((𝜒 → 𝜒) → (¬ ¬ ¬ 𝜑 → ¬ 𝜑)) → ¬ ¬ 𝜑) → 𝜓))
3		merlem13 1686	. . . 4 ⊢ (((𝜑 → 𝜓) → ((((𝜒 → 𝜒) → (¬ ¬ ¬ 𝜑 → ¬ 𝜑)) → ¬ ¬ 𝜑) → 𝜓)) → ((((((𝜓 → 𝜒) → (𝜑 → 𝜒)) → 𝜑) → (¬ ¬ ¬ (𝜑 → 𝜓) → ¬ (𝜑 → 𝜓))) → ¬ ¬ (𝜑 → 𝜓)) → ((((𝜒 → 𝜒) → (¬ ¬ ¬ 𝜑 → ¬ 𝜑)) → ¬ ¬ 𝜑) → 𝜓)))
4	2, 3	ax-mp 5	. . 3 ⊢ ((((((𝜓 → 𝜒) → (𝜑 → 𝜒)) → 𝜑) → (¬ ¬ ¬ (𝜑 → 𝜓) → ¬ (𝜑 → 𝜓))) → ¬ ¬ (𝜑 → 𝜓)) → ((((𝜒 → 𝜒) → (¬ ¬ ¬ 𝜑 → ¬ 𝜑)) → ¬ ¬ 𝜑) → 𝜓))
5		meredith 1673	. . 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-1 6  ax-2 7  ax-3 8

This theorem is used by:  luklem1  1690  luklem2  1691  luklem4  1693  luklem6  1695  luklem7  1696  luklem8  1697