Theorem ax2 1670

Description: Standard propositional axiom derived from Lukasiewicz axioms. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
ax2	⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒)))

Proof of Theorem ax2

Step	Hyp	Ref	Expression
1		luklem7 1667	. 2 ⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (𝜑 → 𝜒)))
2		luklem8 1668	. . 3 ⊢ ((𝜓 → (𝜑 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → (𝜑 → 𝜒))))
3		luklem6 1666	. . . 4 ⊢ ((𝜑 → (𝜑 → 𝜒)) → (𝜑 → 𝜒))
4		luklem8 1668	. . . 4 ⊢ (((𝜑 → (𝜑 → 𝜒)) → (𝜑 → 𝜒)) → (((𝜑 → 𝜓) → (𝜑 → (𝜑 → 𝜒))) → ((𝜑 → 𝜓) → (𝜑 → 𝜒))))
5	3, 4	ax-mp 5	. . 3 ⊢ (((𝜑 → 𝜓) → (𝜑 → (𝜑 → 𝜒))) → ((𝜑 → 𝜓) → (𝜑 → 𝜒)))
6	2, 5	luklem1 1661	. 2 ⊢ ((𝜓 → (𝜑 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒)))
7	1, 6	luklem1 1661	1 ⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒)))

Syntax hints:   → wi 4

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

This theorem is referenced by: (None)