Theorem nic-ax 1589

Description: Nicod's axiom derived from the standard ones. See Introduction to Mathematical Philosophy by B. Russell, p. 152. Like meredith 1557, the usual axioms can be derived from this and vice versa. Unlike meredith 1557, Nicod uses a different connective ('nand'), so another form of modus ponens must be used in proofs, e.g. { nic-ax 1589, nic-mp 1587 } is equivalent to { luk-1 1571, luk-2 1572, luk-3 1573, ax-mp 5 }. In a pure (standalone) treatment of Nicod's axiom, this theorem would be changed to an axiom ($a statement). (Contributed by Jeff Hoffman, 19-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
nic-ax	⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⊼ ((𝜏 ⊼ (𝜏 ⊼ 𝜏)) ⊼ ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃)))))

Proof of Theorem nic-ax

Step	Hyp	Ref	Expression
1		nannan 1443	. . . . 5 ⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ↔ (𝜑 → (𝜒 ∧ 𝜓)))
2	1	biimpi 205	. . . 4 ⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) → (𝜑 → (𝜒 ∧ 𝜓)))
3		simpl 472	. . . . 5 ⊢ ((𝜒 ∧ 𝜓) → 𝜒)
4	3	imim2i 16	. . . 4 ⊢ ((𝜑 → (𝜒 ∧ 𝜓)) → (𝜑 → 𝜒))
5		imnan 437	. . . . . . 7 ⊢ ((𝜃 → ¬ 𝜒) ↔ ¬ (𝜃 ∧ 𝜒))
6		df-nan 1440	. . . . . . 7 ⊢ ((𝜃 ⊼ 𝜒) ↔ ¬ (𝜃 ∧ 𝜒))
7	5, 6	bitr4i 266	. . . . . 6 ⊢ ((𝜃 → ¬ 𝜒) ↔ (𝜃 ⊼ 𝜒))
8		con3 148	. . . . . . . 8 ⊢ ((𝜑 → 𝜒) → (¬ 𝜒 → ¬ 𝜑))
9	8	imim2d 55	. . . . . . 7 ⊢ ((𝜑 → 𝜒) → ((𝜃 → ¬ 𝜒) → (𝜃 → ¬ 𝜑)))
10		imnan 437	. . . . . . . 8 ⊢ ((𝜑 → ¬ 𝜃) ↔ ¬ (𝜑 ∧ 𝜃))
11		con2b 348	. . . . . . . 8 ⊢ ((𝜃 → ¬ 𝜑) ↔ (𝜑 → ¬ 𝜃))
12		df-nan 1440	. . . . . . . 8 ⊢ ((𝜑 ⊼ 𝜃) ↔ ¬ (𝜑 ∧ 𝜃))
13	10, 11, 12	3bitr4ri 292	. . . . . . 7 ⊢ ((𝜑 ⊼ 𝜃) ↔ (𝜃 → ¬ 𝜑))
14	9, 13	syl6ibr 241	. . . . . 6 ⊢ ((𝜑 → 𝜒) → ((𝜃 → ¬ 𝜒) → (𝜑 ⊼ 𝜃)))
15	7, 14	syl5bir 232	. . . . 5 ⊢ ((𝜑 → 𝜒) → ((𝜃 ⊼ 𝜒) → (𝜑 ⊼ 𝜃)))
16		nanim 1444	. . . . 5 ⊢ (((𝜃 ⊼ 𝜒) → (𝜑 ⊼ 𝜃)) ↔ ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))
17	15, 16	sylib 207	. . . 4 ⊢ ((𝜑 → 𝜒) → ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))
18	2, 4, 17	3syl 18	. . 3 ⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) → ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))
19		pm4.24 673	. . . . 5 ⊢ (𝜏 ↔ (𝜏 ∧ 𝜏))
20	19	biimpi 205	. . . 4 ⊢ (𝜏 → (𝜏 ∧ 𝜏))
21		nannan 1443	. . . 4 ⊢ ((𝜏 ⊼ (𝜏 ⊼ 𝜏)) ↔ (𝜏 → (𝜏 ∧ 𝜏)))
22	20, 21	mpbir 220	. . 3 ⊢ (𝜏 ⊼ (𝜏 ⊼ 𝜏))
23	18, 22	jctil 558	. 2 ⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) → ((𝜏 ⊼ (𝜏 ⊼ 𝜏)) ∧ ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃)))))
24		nannan 1443	. 2 ⊢ (((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⊼ ((𝜏 ⊼ (𝜏 ⊼ 𝜏)) ⊼ ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))) ↔ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) → ((𝜏 ⊼ (𝜏 ⊼ 𝜏)) ∧ ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))))
25	23, 24	mpbir 220	1 ⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⊼ ((𝜏 ⊼ (𝜏 ⊼ 𝜏)) ⊼ ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃)))))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   ⊼ wnan 1439

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 196  df-an 385  df-nan 1440

This theorem is referenced by:  nic-imp  1591  nic-idlem1  1592  nic-idlem2  1593  nic-id  1594  nic-swap  1595  nic-luk1  1607  lukshef-ax1  1610