Theorem nic-ax 1705

Description: Nicod's axiom derived from the standard ones. See Introduction to Mathematical Philosophy by B. Russell, p. 152. Like meredith 1673, the usual axioms can be derived from this and vice versa. Unlike meredith 1673, Nicod uses a different connective ('nand'), so another form of modus ponens must be used in proofs, e.g., { nic-ax 1705, nic-mp 1703 } is equivalent to { luk-1 1687, luk-2 1688, luk-3 1689, 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 1526	. . . . 5 ⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ↔ (𝜑 → (𝜒 ∧ 𝜓)))
2	1	biimpi 219	. . . 4 ⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) → (𝜑 → (𝜒 ∧ 𝜓)))
3		simpl 488	. . . . 5 ⊢ ((𝜒 ∧ 𝜓) → 𝜒)
4	3	imim2i 17	. . . 4 ⊢ ((𝜑 → (𝜒 ∧ 𝜓)) → (𝜑 → 𝜒))
5		imnan 405	. . . . . . 7 ⊢ ((𝜃 → ¬ 𝜒) ↔ ¬ (𝜃 ∧ 𝜒))
6		df-nan 1521	. . . . . . 7 ⊢ ((𝜃 ⊼ 𝜒) ↔ ¬ (𝜃 ∧ 𝜒))
7	5, 6	bitr4i 281	. . . . . 6 ⊢ ((𝜃 → ¬ 𝜒) ↔ (𝜃 ⊼ 𝜒))
8		con3 154	. . . . . . . 8 ⊢ ((𝜑 → 𝜒) → (¬ 𝜒 → ¬ 𝜑))
9	8	imim2d 58	. . . . . . 7 ⊢ ((𝜑 → 𝜒) → ((𝜃 → ¬ 𝜒) → (𝜃 → ¬ 𝜑)))
10		imnan 405	. . . . . . . 8 ⊢ ((𝜑 → ¬ 𝜃) ↔ ¬ (𝜑 ∧ 𝜃))
11		con2b 362	. . . . . . . 8 ⊢ ((𝜃 → ¬ 𝜑) ↔ (𝜑 → ¬ 𝜃))
12		df-nan 1521	. . . . . . . 8 ⊢ ((𝜑 ⊼ 𝜃) ↔ ¬ (𝜑 ∧ 𝜃))
13	10, 11, 12	3bitr4ri 307	. . . . . . 7 ⊢ ((𝜑 ⊼ 𝜃) ↔ (𝜃 → ¬ 𝜑))
14	9, 13	imbitrrdi 255	. . . . . 6 ⊢ ((𝜑 → 𝜒) → ((𝜃 → ¬ 𝜒) → (𝜑 ⊼ 𝜃)))
15	7, 14	biimtrrid 246	. . . . 5 ⊢ ((𝜑 → 𝜒) → ((𝜃 ⊼ 𝜒) → (𝜑 ⊼ 𝜃)))
16		nanim 1527	. . . . 5 ⊢ (((𝜃 ⊼ 𝜒) → (𝜑 ⊼ 𝜃)) ↔ ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))
17	15, 16	sylib 221	. . . 4 ⊢ ((𝜑 → 𝜒) → ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))
18	2, 4, 17	3syl 19	. . 3 ⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) → ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))
19		pm4.24 574	. . . . 5 ⊢ (𝜏 ↔ (𝜏 ∧ 𝜏))
20	19	biimpi 219	. . . 4 ⊢ (𝜏 → (𝜏 ∧ 𝜏))
21		nannan 1526	. . . 4 ⊢ ((𝜏 ⊼ (𝜏 ⊼ 𝜏)) ↔ (𝜏 → (𝜏 ∧ 𝜏)))
22	20, 21	mpbir 234	. . 3 ⊢ (𝜏 ⊼ (𝜏 ⊼ 𝜏))
23	18, 22	jctil 529	. 2 ⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) → ((𝜏 ⊼ (𝜏 ⊼ 𝜏)) ∧ ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃)))))
24		nannan 1526	. 2 ⊢ (((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⊼ ((𝜏 ⊼ (𝜏 ⊼ 𝜏)) ⊼ ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))) ↔ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) → ((𝜏 ⊼ (𝜏 ⊼ 𝜏)) ∧ ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))))
25	23, 24	mpbir 234	1 ⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⊼ ((𝜏 ⊼ (𝜏 ⊼ 𝜏)) ⊼ ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃)))))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ⊼ wnan 1520

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-nan 1521

This theorem is used by:  nic-imp  1707  nic-idlem1  1708  nic-idlem2  1709  nic-id  1710  nic-swap  1711  nic-luk1  1723  lukshef-ax1  1726