Theorem nic-luk1 1694

Description: Proof of luk-1 1658 from nic-ax 1676 and nic-mp 1674 (and Definitions nic-dfim 1672 and nic-dfneg 1673). Note that the standard axioms ax-1 6, ax-2 7, and ax-3 8 are proved from the Lukasiewicz axioms by Theorems ax1 1669, ax2 1670, and ax3 1671. (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 1672	. . . 4 ⊢ (((𝜑 ⊼ (𝜓 ⊼ 𝜓)) ⊼ (𝜑 → 𝜓)) ⊼ (((𝜑 ⊼ (𝜓 ⊼ 𝜓)) ⊼ (𝜑 ⊼ (𝜓 ⊼ 𝜓))) ⊼ ((𝜑 → 𝜓) ⊼ (𝜑 → 𝜓))))
2	1	nic-bi2 1692	. . 3 ⊢ ((𝜑 → 𝜓) ⊼ ((𝜑 ⊼ (𝜓 ⊼ 𝜓)) ⊼ (𝜑 ⊼ (𝜓 ⊼ 𝜓))))
3		nic-ax 1676	. . . . . . 7 ⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜓)) ⊼ ((𝜏 ⊼ (𝜏 ⊼ 𝜏)) ⊼ (((𝜒 ⊼ 𝜒) ⊼ 𝜓) ⊼ ((𝜑 ⊼ (𝜒 ⊼ 𝜒)) ⊼ (𝜑 ⊼ (𝜒 ⊼ 𝜒))))))
4	3	nic-isw2 1684	. . . . . 6 ⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜓)) ⊼ ((((𝜒 ⊼ 𝜒) ⊼ 𝜓) ⊼ ((𝜑 ⊼ (𝜒 ⊼ 𝜒)) ⊼ (𝜑 ⊼ (𝜒 ⊼ 𝜒)))) ⊼ (𝜏 ⊼ (𝜏 ⊼ 𝜏))))
5	4	nic-idel 1687	. . . . 5 ⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜓)) ⊼ ((((𝜒 ⊼ 𝜒) ⊼ 𝜓) ⊼ ((𝜑 ⊼ (𝜒 ⊼ 𝜒)) ⊼ (𝜑 ⊼ (𝜒 ⊼ 𝜒)))) ⊼ (((𝜒 ⊼ 𝜒) ⊼ 𝜓) ⊼ ((𝜑 ⊼ (𝜒 ⊼ 𝜒)) ⊼ (𝜑 ⊼ (𝜒 ⊼ 𝜒))))))
6		nic-dfim 1672	. . . . . . . . 9 ⊢ (((𝜑 ⊼ (𝜒 ⊼ 𝜒)) ⊼ (𝜑 → 𝜒)) ⊼ (((𝜑 ⊼ (𝜒 ⊼ 𝜒)) ⊼ (𝜑 ⊼ (𝜒 ⊼ 𝜒))) ⊼ ((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒))))
7	6	nic-bi1 1691	. . . . . . . 8 ⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜒)) ⊼ ((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒)))
8	7	nic-idbl 1689	. . . . . . 7 ⊢ (((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒)) ⊼ (((𝜑 ⊼ (𝜒 ⊼ 𝜒)) ⊼ (𝜑 ⊼ (𝜒 ⊼ 𝜒))) ⊼ ((𝜑 ⊼ (𝜒 ⊼ 𝜒)) ⊼ (𝜑 ⊼ (𝜒 ⊼ 𝜒)))))
9	8	nic-imp 1678	. . . . . 6 ⊢ ((((𝜒 ⊼ 𝜒) ⊼ 𝜓) ⊼ ((𝜑 ⊼ (𝜒 ⊼ 𝜒)) ⊼ (𝜑 ⊼ (𝜒 ⊼ 𝜒)))) ⊼ ((((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒)) ⊼ ((𝜒 ⊼ 𝜒) ⊼ 𝜓)) ⊼ (((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒)) ⊼ ((𝜒 ⊼ 𝜒) ⊼ 𝜓))))
10		nic-dfim 1672	. . . . . . . . 9 ⊢ (((𝜓 ⊼ (𝜒 ⊼ 𝜒)) ⊼ (𝜓 → 𝜒)) ⊼ (((𝜓 ⊼ (𝜒 ⊼ 𝜒)) ⊼ (𝜓 ⊼ (𝜒 ⊼ 𝜒))) ⊼ ((𝜓 → 𝜒) ⊼ (𝜓 → 𝜒))))
11	10	nic-bi2 1692	. . . . . . . 8 ⊢ ((𝜓 → 𝜒) ⊼ ((𝜓 ⊼ (𝜒 ⊼ 𝜒)) ⊼ (𝜓 ⊼ (𝜒 ⊼ 𝜒))))
12		nic-swap 1682	. . . . . . . 8 ⊢ ((𝜓 ⊼ (𝜒 ⊼ 𝜒)) ⊼ (((𝜒 ⊼ 𝜒) ⊼ 𝜓) ⊼ ((𝜒 ⊼ 𝜒) ⊼ 𝜓)))
13	11, 12	nic-ich 1688	. . . . . . 7 ⊢ ((𝜓 → 𝜒) ⊼ (((𝜒 ⊼ 𝜒) ⊼ 𝜓) ⊼ ((𝜒 ⊼ 𝜒) ⊼ 𝜓)))
14	13	nic-imp 1678	. . . . . 6 ⊢ ((((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒)) ⊼ ((𝜒 ⊼ 𝜒) ⊼ 𝜓)) ⊼ (((𝜓 → 𝜒) ⊼ ((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒))) ⊼ ((𝜓 → 𝜒) ⊼ ((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒)))))
15	9, 14	nic-ich 1688	. . . . 5 ⊢ ((((𝜒 ⊼ 𝜒) ⊼ 𝜓) ⊼ ((𝜑 ⊼ (𝜒 ⊼ 𝜒)) ⊼ (𝜑 ⊼ (𝜒 ⊼ 𝜒)))) ⊼ (((𝜓 → 𝜒) ⊼ ((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒))) ⊼ ((𝜓 → 𝜒) ⊼ ((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒)))))
16	5, 15	nic-ich 1688	. . . 4 ⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜓)) ⊼ (((𝜓 → 𝜒) ⊼ ((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒))) ⊼ ((𝜓 → 𝜒) ⊼ ((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒)))))
17		nic-dfim 1672	. . . . 5 ⊢ ((((𝜓 → 𝜒) ⊼ ((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒))) ⊼ ((𝜓 → 𝜒) → (𝜑 → 𝜒))) ⊼ ((((𝜓 → 𝜒) ⊼ ((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒))) ⊼ ((𝜓 → 𝜒) ⊼ ((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒)))) ⊼ (((𝜓 → 𝜒) → (𝜑 → 𝜒)) ⊼ ((𝜓 → 𝜒) → (𝜑 → 𝜒)))))
18	17	nic-bi1 1691	. . . 4 ⊢ (((𝜓 → 𝜒) ⊼ ((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒))) ⊼ (((𝜓 → 𝜒) → (𝜑 → 𝜒)) ⊼ ((𝜓 → 𝜒) → (𝜑 → 𝜒))))
19	16, 18	nic-ich 1688	. . 3 ⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜓)) ⊼ (((𝜓 → 𝜒) → (𝜑 → 𝜒)) ⊼ ((𝜓 → 𝜒) → (𝜑 → 𝜒))))
20	2, 19	nic-ich 1688	. 2 ⊢ ((𝜑 → 𝜓) ⊼ (((𝜓 → 𝜒) → (𝜑 → 𝜒)) ⊼ ((𝜓 → 𝜒) → (𝜑 → 𝜒))))
21		nic-dfim 1672	. . 3 ⊢ ((((𝜑 → 𝜓) ⊼ (((𝜓 → 𝜒) → (𝜑 → 𝜒)) ⊼ ((𝜓 → 𝜒) → (𝜑 → 𝜒)))) ⊼ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒)))) ⊼ ((((𝜑 → 𝜓) ⊼ (((𝜓 → 𝜒) → (𝜑 → 𝜒)) ⊼ ((𝜓 → 𝜒) → (𝜑 → 𝜒)))) ⊼ ((𝜑 → 𝜓) ⊼ (((𝜓 → 𝜒) → (𝜑 → 𝜒)) ⊼ ((𝜓 → 𝜒) → (𝜑 → 𝜒))))) ⊼ (((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒))) ⊼ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒))))))
22	21	nic-bi1 1691	. 2 ⊢ (((𝜑 → 𝜓) ⊼ (((𝜓 → 𝜒) → (𝜑 → 𝜒)) ⊼ ((𝜓 → 𝜒) → (𝜑 → 𝜒)))) ⊼ (((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒))) ⊼ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒)))))
23	20, 22	nic-mp 1674	1 ⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒)))

Syntax hints:   → wi 4   ⊼ wnan 1486

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 206  df-an 397  df-or 845  df-nan 1487

This theorem is referenced by: (None)