Theorem nic-ax 1673

Description: Nicod's axiom derived from the standard ones. See Introduction to Mathematical Philosophy by B. Russell, p. 152. Like meredith 1641, the usual axioms can be derived from this and vice versa. Unlike meredith 1641, Nicod uses a different connective ('nand'), so another form of modus ponens must be used in proofs, e.g., { nic-ax 1673, nic-mp 1671 } is equivalent to { luk-1 1655, luk-2 1656, luk-3 1657, 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 1497	. . . . 5 ⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ↔ (𝜑 → (𝜒 ∧ 𝜓)))
2	1	biimpi 216	. . . 4 ⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) → (𝜑 → (𝜒 ∧ 𝜓)))
3		simpl 482	. . . . 5 ⊢ ((𝜒 ∧ 𝜓) → 𝜒)
4	3	imim2i 16	. . . 4 ⊢ ((𝜑 → (𝜒 ∧ 𝜓)) → (𝜑 → 𝜒))
5		imnan 399	. . . . . . 7 ⊢ ((𝜃 → ¬ 𝜒) ↔ ¬ (𝜃 ∧ 𝜒))
6		df-nan 1492	. . . . . . 7 ⊢ ((𝜃 ⊼ 𝜒) ↔ ¬ (𝜃 ∧ 𝜒))
7	5, 6	bitr4i 278	. . . . . 6 ⊢ ((𝜃 → ¬ 𝜒) ↔ (𝜃 ⊼ 𝜒))
8		con3 153	. . . . . . . 8 ⊢ ((𝜑 → 𝜒) → (¬ 𝜒 → ¬ 𝜑))
9	8	imim2d 57	. . . . . . 7 ⊢ ((𝜑 → 𝜒) → ((𝜃 → ¬ 𝜒) → (𝜃 → ¬ 𝜑)))
10		imnan 399	. . . . . . . 8 ⊢ ((𝜑 → ¬ 𝜃) ↔ ¬ (𝜑 ∧ 𝜃))
11		con2b 359	. . . . . . . 8 ⊢ ((𝜃 → ¬ 𝜑) ↔ (𝜑 → ¬ 𝜃))
12		df-nan 1492	. . . . . . . 8 ⊢ ((𝜑 ⊼ 𝜃) ↔ ¬ (𝜑 ∧ 𝜃))
13	10, 11, 12	3bitr4ri 304	. . . . . . 7 ⊢ ((𝜑 ⊼ 𝜃) ↔ (𝜃 → ¬ 𝜑))
14	9, 13	imbitrrdi 252	. . . . . 6 ⊢ ((𝜑 → 𝜒) → ((𝜃 → ¬ 𝜒) → (𝜑 ⊼ 𝜃)))
15	7, 14	biimtrrid 243	. . . . 5 ⊢ ((𝜑 → 𝜒) → ((𝜃 ⊼ 𝜒) → (𝜑 ⊼ 𝜃)))
16		nanim 1498	. . . . 5 ⊢ (((𝜃 ⊼ 𝜒) → (𝜑 ⊼ 𝜃)) ↔ ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))
17	15, 16	sylib 218	. . . 4 ⊢ ((𝜑 → 𝜒) → ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))
18	2, 4, 17	3syl 18	. . 3 ⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) → ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))
19		pm4.24 563	. . . . 5 ⊢ (𝜏 ↔ (𝜏 ∧ 𝜏))
20	19	biimpi 216	. . . 4 ⊢ (𝜏 → (𝜏 ∧ 𝜏))
21		nannan 1497	. . . 4 ⊢ ((𝜏 ⊼ (𝜏 ⊼ 𝜏)) ↔ (𝜏 → (𝜏 ∧ 𝜏)))
22	20, 21	mpbir 231	. . 3 ⊢ (𝜏 ⊼ (𝜏 ⊼ 𝜏))
23	18, 22	jctil 519	. 2 ⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) → ((𝜏 ⊼ (𝜏 ⊼ 𝜏)) ∧ ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃)))))
24		nannan 1497	. 2 ⊢ (((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⊼ ((𝜏 ⊼ (𝜏 ⊼ 𝜏)) ⊼ ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))) ↔ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) → ((𝜏 ⊼ (𝜏 ⊼ 𝜏)) ∧ ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))))
25	23, 24	mpbir 231	1 ⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⊼ ((𝜏 ⊼ (𝜏 ⊼ 𝜏)) ⊼ ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃)))))

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

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 207  df-an 396  df-nan 1492

This theorem is referenced by:  nic-imp  1675  nic-idlem1  1676  nic-idlem2  1677  nic-id  1678  nic-swap  1679  nic-luk1  1691  lukshef-ax1  1694