Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nic-ax Structured version   Visualization version   GIF version

Theorem nic-ax 1638
 Description: Nicod's axiom derived from the standard ones. See Introduction to Mathematical Philosophy by B. Russell, p. 152. Like meredith 1606, the usual axioms can be derived from this and vice versa. Unlike meredith 1606, Nicod uses a different connective ('nand'), so another form of modus ponens must be used in proofs, e.g. { nic-ax 1638, nic-mp 1636 } is equivalent to { luk-1 1620, luk-2 1621, luk-3 1622, 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
StepHypRef Expression
1 nannan 1491 . . . . 5 ((𝜑 ⊼ (𝜒𝜓)) ↔ (𝜑 → (𝜒𝜓)))
21biimpi 206 . . . 4 ((𝜑 ⊼ (𝜒𝜓)) → (𝜑 → (𝜒𝜓)))
3 simpl 472 . . . . 5 ((𝜒𝜓) → 𝜒)
43imim2i 16 . . . 4 ((𝜑 → (𝜒𝜓)) → (𝜑𝜒))
5 imnan 437 . . . . . . 7 ((𝜃 → ¬ 𝜒) ↔ ¬ (𝜃𝜒))
6 df-nan 1488 . . . . . . 7 ((𝜃𝜒) ↔ ¬ (𝜃𝜒))
75, 6bitr4i 267 . . . . . 6 ((𝜃 → ¬ 𝜒) ↔ (𝜃𝜒))
8 con3 149 . . . . . . . 8 ((𝜑𝜒) → (¬ 𝜒 → ¬ 𝜑))
98imim2d 57 . . . . . . 7 ((𝜑𝜒) → ((𝜃 → ¬ 𝜒) → (𝜃 → ¬ 𝜑)))
10 imnan 437 . . . . . . . 8 ((𝜑 → ¬ 𝜃) ↔ ¬ (𝜑𝜃))
11 con2b 348 . . . . . . . 8 ((𝜃 → ¬ 𝜑) ↔ (𝜑 → ¬ 𝜃))
12 df-nan 1488 . . . . . . . 8 ((𝜑𝜃) ↔ ¬ (𝜑𝜃))
1310, 11, 123bitr4ri 293 . . . . . . 7 ((𝜑𝜃) ↔ (𝜃 → ¬ 𝜑))
149, 13syl6ibr 242 . . . . . 6 ((𝜑𝜒) → ((𝜃 → ¬ 𝜒) → (𝜑𝜃)))
157, 14syl5bir 233 . . . . 5 ((𝜑𝜒) → ((𝜃𝜒) → (𝜑𝜃)))
16 nanim 1492 . . . . 5 (((𝜃𝜒) → (𝜑𝜃)) ↔ ((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃))))
1715, 16sylib 208 . . . 4 ((𝜑𝜒) → ((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃))))
182, 4, 173syl 18 . . 3 ((𝜑 ⊼ (𝜒𝜓)) → ((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃))))
19 pm4.24 676 . . . . 5 (𝜏 ↔ (𝜏𝜏))
2019biimpi 206 . . . 4 (𝜏 → (𝜏𝜏))
21 nannan 1491 . . . 4 ((𝜏 ⊼ (𝜏𝜏)) ↔ (𝜏 → (𝜏𝜏)))
2220, 21mpbir 221 . . 3 (𝜏 ⊼ (𝜏𝜏))
2318, 22jctil 559 . 2 ((𝜑 ⊼ (𝜒𝜓)) → ((𝜏 ⊼ (𝜏𝜏)) ∧ ((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃)))))
24 nannan 1491 . 2 (((𝜑 ⊼ (𝜒𝜓)) ⊼ ((𝜏 ⊼ (𝜏𝜏)) ⊼ ((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃))))) ↔ ((𝜑 ⊼ (𝜒𝜓)) → ((𝜏 ⊼ (𝜏𝜏)) ∧ ((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃))))))
2523, 24mpbir 221 1 ((𝜑 ⊼ (𝜒𝜓)) ⊼ ((𝜏 ⊼ (𝜏𝜏)) ⊼ ((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃)))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   ⊼ wnan 1487 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 197  df-an 385  df-nan 1488 This theorem is referenced by:  nic-imp  1640  nic-idlem1  1641  nic-idlem2  1642  nic-id  1643  nic-swap  1644  nic-luk1  1656  lukshef-ax1  1659
 Copyright terms: Public domain W3C validator