Theorem luklem4 1690

Description: Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
luklem4	⊢ ((((¬ 𝜑 → 𝜑) → 𝜑) → 𝜓) → 𝜓)

Proof of Theorem luklem4

Step	Hyp	Ref	Expression
1		luk-2 1685	. . . 4 ⊢ ((¬ ((¬ 𝜑 → 𝜑) → 𝜑) → ((¬ 𝜑 → 𝜑) → 𝜑)) → ((¬ 𝜑 → 𝜑) → 𝜑))
2		luk-2 1685	. . . . 5 ⊢ ((¬ 𝜑 → 𝜑) → 𝜑)
3		luklem3 1689	. . . . 5 ⊢ (((¬ 𝜑 → 𝜑) → 𝜑) → (((¬ ((¬ 𝜑 → 𝜑) → 𝜑) → ((¬ 𝜑 → 𝜑) → 𝜑)) → ((¬ 𝜑 → 𝜑) → 𝜑)) → (¬ 𝜓 → ((¬ 𝜑 → 𝜑) → 𝜑))))
4	2, 3	ax-mp 5	. . . 4 ⊢ (((¬ ((¬ 𝜑 → 𝜑) → 𝜑) → ((¬ 𝜑 → 𝜑) → 𝜑)) → ((¬ 𝜑 → 𝜑) → 𝜑)) → (¬ 𝜓 → ((¬ 𝜑 → 𝜑) → 𝜑)))
5	1, 4	ax-mp 5	. . 3 ⊢ (¬ 𝜓 → ((¬ 𝜑 → 𝜑) → 𝜑))
6		luk-1 1684	. . 3 ⊢ ((¬ 𝜓 → ((¬ 𝜑 → 𝜑) → 𝜑)) → ((((¬ 𝜑 → 𝜑) → 𝜑) → 𝜓) → (¬ 𝜓 → 𝜓)))
7	5, 6	ax-mp 5	. 2 ⊢ ((((¬ 𝜑 → 𝜑) → 𝜑) → 𝜓) → (¬ 𝜓 → 𝜓))
8		luk-2 1685	. 2 ⊢ ((¬ 𝜓 → 𝜓) → 𝜓)
9	7, 8	luklem1 1687	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:  luklem5  1691  luklem6  1692  ax3  1697