Theorem nic-ax 1677

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ⊼ wnan 1483

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 396  df-nan 1484

This theorem is referenced by:  nic-imp  1679  nic-idlem1  1680  nic-idlem2  1681  nic-id  1682  nic-swap  1683  nic-luk1  1695  lukshef-ax1  1698