Theorem nic-luk1 1724

Description: Proof of luk-1 1688 from nic-ax 1706 and nic-mp 1704 (and Definitions nic-dfim 1702 and nic-dfneg 1703). Note that the standard axioms ax-1 6, ax-2 7, and ax-3 8 are proved from the Lukasiewicz axioms by Theorems ax1 1699, ax2 1700, and ax3 1701. (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 1702	. . . 4 ⊢ (((𝜑 ⊼ (𝜓 ⊼ 𝜓)) ⊼ (𝜑 → 𝜓)) ⊼ (((𝜑 ⊼ (𝜓 ⊼ 𝜓)) ⊼ (𝜑 ⊼ (𝜓 ⊼ 𝜓))) ⊼ ((𝜑 → 𝜓) ⊼ (𝜑 → 𝜓))))
2	1	nic-bi2 1722	. . 3 ⊢ ((𝜑 → 𝜓) ⊼ ((𝜑 ⊼ (𝜓 ⊼ 𝜓)) ⊼ (𝜑 ⊼ (𝜓 ⊼ 𝜓))))
3		nic-ax 1706	. . . . . . 7 ⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜓)) ⊼ ((𝜏 ⊼ (𝜏 ⊼ 𝜏)) ⊼ (((𝜒 ⊼ 𝜒) ⊼ 𝜓) ⊼ ((𝜑 ⊼ (𝜒 ⊼ 𝜒)) ⊼ (𝜑 ⊼ (𝜒 ⊼ 𝜒))))))
4	3	nic-isw2 1714	. . . . . 6 ⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜓)) ⊼ ((((𝜒 ⊼ 𝜒) ⊼ 𝜓) ⊼ ((𝜑 ⊼ (𝜒 ⊼ 𝜒)) ⊼ (𝜑 ⊼ (𝜒 ⊼ 𝜒)))) ⊼ (𝜏 ⊼ (𝜏 ⊼ 𝜏))))
5	4	nic-idel 1717	. . . . 5 ⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜓)) ⊼ ((((𝜒 ⊼ 𝜒) ⊼ 𝜓) ⊼ ((𝜑 ⊼ (𝜒 ⊼ 𝜒)) ⊼ (𝜑 ⊼ (𝜒 ⊼ 𝜒)))) ⊼ (((𝜒 ⊼ 𝜒) ⊼ 𝜓) ⊼ ((𝜑 ⊼ (𝜒 ⊼ 𝜒)) ⊼ (𝜑 ⊼ (𝜒 ⊼ 𝜒))))))
6		nic-dfim 1702	. . . . . . . . 9 ⊢ (((𝜑 ⊼ (𝜒 ⊼ 𝜒)) ⊼ (𝜑 → 𝜒)) ⊼ (((𝜑 ⊼ (𝜒 ⊼ 𝜒)) ⊼ (𝜑 ⊼ (𝜒 ⊼ 𝜒))) ⊼ ((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒))))
7	6	nic-bi1 1721	. . . . . . . 8 ⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜒)) ⊼ ((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒)))
8	7	nic-idbl 1719	. . . . . . 7 ⊢ (((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒)) ⊼ (((𝜑 ⊼ (𝜒 ⊼ 𝜒)) ⊼ (𝜑 ⊼ (𝜒 ⊼ 𝜒))) ⊼ ((𝜑 ⊼ (𝜒 ⊼ 𝜒)) ⊼ (𝜑 ⊼ (𝜒 ⊼ 𝜒)))))
9	8	nic-imp 1708	. . . . . 6 ⊢ ((((𝜒 ⊼ 𝜒) ⊼ 𝜓) ⊼ ((𝜑 ⊼ (𝜒 ⊼ 𝜒)) ⊼ (𝜑 ⊼ (𝜒 ⊼ 𝜒)))) ⊼ ((((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒)) ⊼ ((𝜒 ⊼ 𝜒) ⊼ 𝜓)) ⊼ (((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒)) ⊼ ((𝜒 ⊼ 𝜒) ⊼ 𝜓))))
10		nic-dfim 1702	. . . . . . . . 9 ⊢ (((𝜓 ⊼ (𝜒 ⊼ 𝜒)) ⊼ (𝜓 → 𝜒)) ⊼ (((𝜓 ⊼ (𝜒 ⊼ 𝜒)) ⊼ (𝜓 ⊼ (𝜒 ⊼ 𝜒))) ⊼ ((𝜓 → 𝜒) ⊼ (𝜓 → 𝜒))))
11	10	nic-bi2 1722	. . . . . . . 8 ⊢ ((𝜓 → 𝜒) ⊼ ((𝜓 ⊼ (𝜒 ⊼ 𝜒)) ⊼ (𝜓 ⊼ (𝜒 ⊼ 𝜒))))
12		nic-swap 1712	. . . . . . . 8 ⊢ ((𝜓 ⊼ (𝜒 ⊼ 𝜒)) ⊼ (((𝜒 ⊼ 𝜒) ⊼ 𝜓) ⊼ ((𝜒 ⊼ 𝜒) ⊼ 𝜓)))
13	11, 12	nic-ich 1718	. . . . . . 7 ⊢ ((𝜓 → 𝜒) ⊼ (((𝜒 ⊼ 𝜒) ⊼ 𝜓) ⊼ ((𝜒 ⊼ 𝜒) ⊼ 𝜓)))
14	13	nic-imp 1708	. . . . . 6 ⊢ ((((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒)) ⊼ ((𝜒 ⊼ 𝜒) ⊼ 𝜓)) ⊼ (((𝜓 → 𝜒) ⊼ ((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒))) ⊼ ((𝜓 → 𝜒) ⊼ ((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒)))))
15	9, 14	nic-ich 1718	. . . . 5 ⊢ ((((𝜒 ⊼ 𝜒) ⊼ 𝜓) ⊼ ((𝜑 ⊼ (𝜒 ⊼ 𝜒)) ⊼ (𝜑 ⊼ (𝜒 ⊼ 𝜒)))) ⊼ (((𝜓 → 𝜒) ⊼ ((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒))) ⊼ ((𝜓 → 𝜒) ⊼ ((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒)))))
16	5, 15	nic-ich 1718	. . . 4 ⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜓)) ⊼ (((𝜓 → 𝜒) ⊼ ((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒))) ⊼ ((𝜓 → 𝜒) ⊼ ((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒)))))
17		nic-dfim 1702	. . . . 5 ⊢ ((((𝜓 → 𝜒) ⊼ ((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒))) ⊼ ((𝜓 → 𝜒) → (𝜑 → 𝜒))) ⊼ ((((𝜓 → 𝜒) ⊼ ((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒))) ⊼ ((𝜓 → 𝜒) ⊼ ((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒)))) ⊼ (((𝜓 → 𝜒) → (𝜑 → 𝜒)) ⊼ ((𝜓 → 𝜒) → (𝜑 → 𝜒)))))
18	17	nic-bi1 1721	. . . 4 ⊢ (((𝜓 → 𝜒) ⊼ ((𝜑 → 𝜒) ⊼ (𝜑 → 𝜒))) ⊼ (((𝜓 → 𝜒) → (𝜑 → 𝜒)) ⊼ ((𝜓 → 𝜒) → (𝜑 → 𝜒))))
19	16, 18	nic-ich 1718	. . 3 ⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜓)) ⊼ (((𝜓 → 𝜒) → (𝜑 → 𝜒)) ⊼ ((𝜓 → 𝜒) → (𝜑 → 𝜒))))
20	2, 19	nic-ich 1718	. 2 ⊢ ((𝜑 → 𝜓) ⊼ (((𝜓 → 𝜒) → (𝜑 → 𝜒)) ⊼ ((𝜓 → 𝜒) → (𝜑 → 𝜒))))
21		nic-dfim 1702	. . 3 ⊢ ((((𝜑 → 𝜓) ⊼ (((𝜓 → 𝜒) → (𝜑 → 𝜒)) ⊼ ((𝜓 → 𝜒) → (𝜑 → 𝜒)))) ⊼ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒)))) ⊼ ((((𝜑 → 𝜓) ⊼ (((𝜓 → 𝜒) → (𝜑 → 𝜒)) ⊼ ((𝜓 → 𝜒) → (𝜑 → 𝜒)))) ⊼ ((𝜑 → 𝜓) ⊼ (((𝜓 → 𝜒) → (𝜑 → 𝜒)) ⊼ ((𝜓 → 𝜒) → (𝜑 → 𝜒))))) ⊼ (((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒))) ⊼ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒))))))
22	21	nic-bi1 1721	. 2 ⊢ (((𝜑 → 𝜓) ⊼ (((𝜓 → 𝜒) → (𝜑 → 𝜒)) ⊼ ((𝜓 → 𝜒) → (𝜑 → 𝜒)))) ⊼ (((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒))) ⊼ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒)))))
23	20, 22	nic-mp 1704	1 ⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒)))

This proof depends on syntax axioms:   → wi 4   ⊼ wnan 1521

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-nan 1522

This theorem is used by: (None)