Theorem nic-ax 1676

Description: Nicod's axiom derived from the standard ones. See Introduction to Mathematical Philosophy by B. Russell, p. 152. Like meredith 1644, the usual axioms can be derived from this and vice versa. Unlike meredith 1644, Nicod uses a different connective ('nand'), so another form of modus ponens must be used in proofs, e.g., { nic-ax 1676, nic-mp 1674 } is equivalent to { luk-1 1658, luk-2 1659, luk-3 1660, 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 1496	. . . . 5 ⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ↔ (𝜑 → (𝜒 ∧ 𝜓)))
2	1	biimpi 215	. . . 4 ⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) → (𝜑 → (𝜒 ∧ 𝜓)))
3		simpl 484	. . . . 5 ⊢ ((𝜒 ∧ 𝜓) → 𝜒)
4	3	imim2i 16	. . . 4 ⊢ ((𝜑 → (𝜒 ∧ 𝜓)) → (𝜑 → 𝜒))
5		imnan 401	. . . . . . 7 ⊢ ((𝜃 → ¬ 𝜒) ↔ ¬ (𝜃 ∧ 𝜒))
6		df-nan 1491	. . . . . . 7 ⊢ ((𝜃 ⊼ 𝜒) ↔ ¬ (𝜃 ∧ 𝜒))
7	5, 6	bitr4i 278	. . . . . 6 ⊢ ((𝜃 → ¬ 𝜒) ↔ (𝜃 ⊼ 𝜒))
8		con3 153	. . . . . . . 8 ⊢ ((𝜑 → 𝜒) → (¬ 𝜒 → ¬ 𝜑))
9	8	imim2d 57	. . . . . . 7 ⊢ ((𝜑 → 𝜒) → ((𝜃 → ¬ 𝜒) → (𝜃 → ¬ 𝜑)))
10		imnan 401	. . . . . . . 8 ⊢ ((𝜑 → ¬ 𝜃) ↔ ¬ (𝜑 ∧ 𝜃))
11		con2b 360	. . . . . . . 8 ⊢ ((𝜃 → ¬ 𝜑) ↔ (𝜑 → ¬ 𝜃))
12		df-nan 1491	. . . . . . . 8 ⊢ ((𝜑 ⊼ 𝜃) ↔ ¬ (𝜑 ∧ 𝜃))
13	10, 11, 12	3bitr4ri 304	. . . . . . 7 ⊢ ((𝜑 ⊼ 𝜃) ↔ (𝜃 → ¬ 𝜑))
14	9, 13	imbitrrdi 251	. . . . . 6 ⊢ ((𝜑 → 𝜒) → ((𝜃 → ¬ 𝜒) → (𝜑 ⊼ 𝜃)))
15	7, 14	biimtrrid 242	. . . . 5 ⊢ ((𝜑 → 𝜒) → ((𝜃 ⊼ 𝜒) → (𝜑 ⊼ 𝜃)))
16		nanim 1497	. . . . 5 ⊢ (((𝜃 ⊼ 𝜒) → (𝜑 ⊼ 𝜃)) ↔ ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))
17	15, 16	sylib 217	. . . 4 ⊢ ((𝜑 → 𝜒) → ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))
18	2, 4, 17	3syl 18	. . 3 ⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) → ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))
19		pm4.24 565	. . . . 5 ⊢ (𝜏 ↔ (𝜏 ∧ 𝜏))
20	19	biimpi 215	. . . 4 ⊢ (𝜏 → (𝜏 ∧ 𝜏))
21		nannan 1496	. . . 4 ⊢ ((𝜏 ⊼ (𝜏 ⊼ 𝜏)) ↔ (𝜏 → (𝜏 ∧ 𝜏)))
22	20, 21	mpbir 230	. . 3 ⊢ (𝜏 ⊼ (𝜏 ⊼ 𝜏))
23	18, 22	jctil 521	. 2 ⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) → ((𝜏 ⊼ (𝜏 ⊼ 𝜏)) ∧ ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃)))))
24		nannan 1496	. 2 ⊢ (((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⊼ ((𝜏 ⊼ (𝜏 ⊼ 𝜏)) ⊼ ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))) ↔ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) → ((𝜏 ⊼ (𝜏 ⊼ 𝜏)) ∧ ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))))
25	23, 24	mpbir 230	1 ⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⊼ ((𝜏 ⊼ (𝜏 ⊼ 𝜏)) ⊼ ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃)))))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 397   ⊼ wnan 1490

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 398  df-nan 1491

This theorem is referenced by:  nic-imp  1678  nic-idlem1  1679  nic-idlem2  1680  nic-id  1681  nic-swap  1682  nic-luk1  1694  lukshef-ax1  1697