Theorem nic-luk1 1688

Description: Proof of luk-1 1652 from nic-ax 1670 and nic-mp 1668 (and definitions nic-dfim 1666 and nic-dfneg 1667). Note that the standard axioms ax-1 6, ax-2 7, and ax-3 8 are proved from the Lukasiewicz axioms by theorems ax1 1663, ax2 1664, and ax3 1665. (Contributed by Jeff Hoffman, 18-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
nic-luk1	⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒)))

Proof of Theorem nic-luk1

Step	Hyp	Ref	Expression
1		nic-dfim 1666	. . . 4 ⊢ (((𝜑 ⊼ (𝜓 ⊼ 𝜓)) ⊼ (𝜑 → 𝜓)) ⊼ (((𝜑 ⊼ (𝜓 ⊼ 𝜓)) ⊼ (𝜑 ⊼ (𝜓 ⊼ 𝜓))) ⊼ ((𝜑 → 𝜓) ⊼ (𝜑 → 𝜓))))
2	1	nic-bi2 1686	. . 3 ⊢ ((𝜑 → 𝜓) ⊼ ((𝜑 ⊼ (𝜓 ⊼ 𝜓)) ⊼ (𝜑 ⊼ (𝜓 ⊼ 𝜓))))
3		nic-ax 1670	. . . . . . 7 ⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜓)) ⊼ ((𝜏 ⊼ (𝜏 ⊼ 𝜏)) ⊼ (((𝜒 ⊼ 𝜒) ⊼ 𝜓) ⊼ ((𝜑 ⊼ (𝜒 ⊼ 𝜒)) ⊼ (𝜑 ⊼ (𝜒 ⊼ 𝜒))))))
4	3	nic-isw2 1678	. . . . . 6 ⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜓)) ⊼ ((((𝜒 ⊼ 𝜒) ⊼ 𝜓) ⊼ ((𝜑 ⊼ (𝜒 ⊼ 𝜒)) ⊼ (𝜑 ⊼ (𝜒 ⊼ 𝜒)))) ⊼ (𝜏 ⊼ (𝜏 ⊼ 𝜏))))
5	4	nic-idel 1681	. . . . 5 ⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜓)) ⊼ ((((𝜒 ⊼ 𝜒) ⊼ 𝜓) ⊼ ((𝜑 ⊼ (𝜒 ⊼ 𝜒)) ⊼ (𝜑 ⊼ (𝜒 ⊼ 𝜒)))) ⊼ (((𝜒 ⊼ 𝜒) ⊼ 𝜓) ⊼ ((𝜑 ⊼ (𝜒 ⊼ 𝜒)) ⊼ (𝜑 ⊼ (𝜒 ⊼ 𝜒))))))
6		nic-dfim 1666	. . . . . . . . 9 ⊢ (((𝜑 ⊼ (𝜒 ⊼ 𝜒)) ⊼ (𝜑 → 𝜒)) ⊼ (((𝜑 ⊼ (𝜒 ⊼ 𝜒)) ⊼ (𝜑 ⊼ (𝜒 ⊼ 𝜒))) ⊼ ((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒))))
7	6	nic-bi1 1685	. . . . . . . 8 ⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜒)) ⊼ ((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒)))
8	7	nic-idbl 1683	. . . . . . 7 ⊢ (((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒)) ⊼ (((𝜑 ⊼ (𝜒 ⊼ 𝜒)) ⊼ (𝜑 ⊼ (𝜒 ⊼ 𝜒))) ⊼ ((𝜑 ⊼ (𝜒 ⊼ 𝜒)) ⊼ (𝜑 ⊼ (𝜒 ⊼ 𝜒)))))
9	8	nic-imp 1672	. . . . . 6 ⊢ ((((𝜒 ⊼ 𝜒) ⊼ 𝜓) ⊼ ((𝜑 ⊼ (𝜒 ⊼ 𝜒)) ⊼ (𝜑 ⊼ (𝜒 ⊼ 𝜒)))) ⊼ ((((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒)) ⊼ ((𝜒 ⊼ 𝜒) ⊼ 𝜓)) ⊼ (((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒)) ⊼ ((𝜒 ⊼ 𝜒) ⊼ 𝜓))))
10		nic-dfim 1666	. . . . . . . . 9 ⊢ (((𝜓 ⊼ (𝜒 ⊼ 𝜒)) ⊼ (𝜓 → 𝜒)) ⊼ (((𝜓 ⊼ (𝜒 ⊼ 𝜒)) ⊼ (𝜓 ⊼ (𝜒 ⊼ 𝜒))) ⊼ ((𝜓 → 𝜒) ⊼ (𝜓 → 𝜒))))
11	10	nic-bi2 1686	. . . . . . . 8 ⊢ ((𝜓 → 𝜒) ⊼ ((𝜓 ⊼ (𝜒 ⊼ 𝜒)) ⊼ (𝜓 ⊼ (𝜒 ⊼ 𝜒))))
12		nic-swap 1676	. . . . . . . 8 ⊢ ((𝜓 ⊼ (𝜒 ⊼ 𝜒)) ⊼ (((𝜒 ⊼ 𝜒) ⊼ 𝜓) ⊼ ((𝜒 ⊼ 𝜒) ⊼ 𝜓)))
13	11, 12	nic-ich 1682	. . . . . . 7 ⊢ ((𝜓 → 𝜒) ⊼ (((𝜒 ⊼ 𝜒) ⊼ 𝜓) ⊼ ((𝜒 ⊼ 𝜒) ⊼ 𝜓)))
14	13	nic-imp 1672	. . . . . 6 ⊢ ((((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒)) ⊼ ((𝜒 ⊼ 𝜒) ⊼ 𝜓)) ⊼ (((𝜓 → 𝜒) ⊼ ((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒))) ⊼ ((𝜓 → 𝜒) ⊼ ((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒)))))
15	9, 14	nic-ich 1682	. . . . 5 ⊢ ((((𝜒 ⊼ 𝜒) ⊼ 𝜓) ⊼ ((𝜑 ⊼ (𝜒 ⊼ 𝜒)) ⊼ (𝜑 ⊼ (𝜒 ⊼ 𝜒)))) ⊼ (((𝜓 → 𝜒) ⊼ ((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒))) ⊼ ((𝜓 → 𝜒) ⊼ ((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒)))))
16	5, 15	nic-ich 1682	. . . 4 ⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜓)) ⊼ (((𝜓 → 𝜒) ⊼ ((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒))) ⊼ ((𝜓 → 𝜒) ⊼ ((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒)))))
17		nic-dfim 1666	. . . . 5 ⊢ ((((𝜓 → 𝜒) ⊼ ((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒))) ⊼ ((𝜓 → 𝜒) → (𝜑 → 𝜒))) ⊼ ((((𝜓 → 𝜒) ⊼ ((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒))) ⊼ ((𝜓 → 𝜒) ⊼ ((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒)))) ⊼ (((𝜓 → 𝜒) → (𝜑 → 𝜒)) ⊼ ((𝜓 → 𝜒) → (𝜑 → 𝜒)))))
18	17	nic-bi1 1685	. . . 4 ⊢ (((𝜓 → 𝜒) ⊼ ((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒))) ⊼ (((𝜓 → 𝜒) → (𝜑 → 𝜒)) ⊼ ((𝜓 → 𝜒) → (𝜑 → 𝜒))))
19	16, 18	nic-ich 1682	. . 3 ⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜓)) ⊼ (((𝜓 → 𝜒) → (𝜑 → 𝜒)) ⊼ ((𝜓 → 𝜒) → (𝜑 → 𝜒))))
20	2, 19	nic-ich 1682	. 2 ⊢ ((𝜑 → 𝜓) ⊼ (((𝜓 → 𝜒) → (𝜑 → 𝜒)) ⊼ ((𝜓 → 𝜒) → (𝜑 → 𝜒))))
21		nic-dfim 1666	. . 3 ⊢ ((((𝜑 → 𝜓) ⊼ (((𝜓 → 𝜒) → (𝜑 → 𝜒)) ⊼ ((𝜓 → 𝜒) → (𝜑 → 𝜒)))) ⊼ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒)))) ⊼ ((((𝜑 → 𝜓) ⊼ (((𝜓 → 𝜒) → (𝜑 → 𝜒)) ⊼ ((𝜓 → 𝜒) → (𝜑 → 𝜒)))) ⊼ ((𝜑 → 𝜓) ⊼ (((𝜓 → 𝜒) → (𝜑 → 𝜒)) ⊼ ((𝜓 → 𝜒) → (𝜑 → 𝜒))))) ⊼ (((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒))) ⊼ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒))))))
22	21	nic-bi1 1685	. 2 ⊢ (((𝜑 → 𝜓) ⊼ (((𝜓 → 𝜒) → (𝜑 → 𝜒)) ⊼ ((𝜓 → 𝜒) → (𝜑 → 𝜒)))) ⊼ (((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒))) ⊼ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒)))))
23	20, 22	nic-mp 1668	1 ⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒)))

Syntax hints:   → wi 4   ⊼ wnan 1480

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

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-nan 1481

This theorem is referenced by: (None)