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

Theorem nic-ax 1768
Description: Nicod's axiom derived from the standard ones. See Introduction to Mathematical Philosophy by B. Russell, p. 152. Like meredith 1736, the usual axioms can be derived from this and vice versa. Unlike meredith 1736, Nicod uses a different connective ('nand'), so another form of modus ponens must be used in proofs, e.g. { nic-ax 1768, nic-mp 1766 } is equivalent to { luk-1 1750, luk-2 1751, luk-3 1752, 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 1615 . . . . 5 ((𝜑 ⊼ (𝜒𝜓)) ↔ (𝜑 → (𝜒𝜓)))
21biimpi 207 . . . 4 ((𝜑 ⊼ (𝜒𝜓)) → (𝜑 → (𝜒𝜓)))
3 simpl 474 . . . . 5 ((𝜒𝜓) → 𝜒)
43imim2i 16 . . . 4 ((𝜑 → (𝜒𝜓)) → (𝜑𝜒))
5 imnan 388 . . . . . . 7 ((𝜃 → ¬ 𝜒) ↔ ¬ (𝜃𝜒))
6 df-nan 1609 . . . . . . 7 ((𝜃𝜒) ↔ ¬ (𝜃𝜒))
75, 6bitr4i 269 . . . . . 6 ((𝜃 → ¬ 𝜒) ↔ (𝜃𝜒))
8 con3 150 . . . . . . . 8 ((𝜑𝜒) → (¬ 𝜒 → ¬ 𝜑))
98imim2d 57 . . . . . . 7 ((𝜑𝜒) → ((𝜃 → ¬ 𝜒) → (𝜃 → ¬ 𝜑)))
10 imnan 388 . . . . . . . 8 ((𝜑 → ¬ 𝜃) ↔ ¬ (𝜑𝜃))
11 con2b 350 . . . . . . . 8 ((𝜃 → ¬ 𝜑) ↔ (𝜑 → ¬ 𝜃))
12 df-nan 1609 . . . . . . . 8 ((𝜑𝜃) ↔ ¬ (𝜑𝜃))
1310, 11, 123bitr4ri 295 . . . . . . 7 ((𝜑𝜃) ↔ (𝜃 → ¬ 𝜑))
149, 13syl6ibr 243 . . . . . 6 ((𝜑𝜒) → ((𝜃 → ¬ 𝜒) → (𝜑𝜃)))
157, 14syl5bir 234 . . . . 5 ((𝜑𝜒) → ((𝜃𝜒) → (𝜑𝜃)))
16 nanim 1617 . . . . 5 (((𝜃𝜒) → (𝜑𝜃)) ↔ ((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃))))
1715, 16sylib 209 . . . 4 ((𝜑𝜒) → ((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃))))
182, 4, 173syl 18 . . 3 ((𝜑 ⊼ (𝜒𝜓)) → ((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃))))
19 pm4.24 559 . . . . 5 (𝜏 ↔ (𝜏𝜏))
2019biimpi 207 . . . 4 (𝜏 → (𝜏𝜏))
21 nannan 1615 . . . 4 ((𝜏 ⊼ (𝜏𝜏)) ↔ (𝜏 → (𝜏𝜏)))
2220, 21mpbir 222 . . 3 (𝜏 ⊼ (𝜏𝜏))
2318, 22jctil 515 . 2 ((𝜑 ⊼ (𝜒𝜓)) → ((𝜏 ⊼ (𝜏𝜏)) ∧ ((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃)))))
24 nannan 1615 . 2 (((𝜑 ⊼ (𝜒𝜓)) ⊼ ((𝜏 ⊼ (𝜏𝜏)) ⊼ ((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃))))) ↔ ((𝜑 ⊼ (𝜒𝜓)) → ((𝜏 ⊼ (𝜏𝜏)) ∧ ((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃))))))
2523, 24mpbir 222 1 ((𝜑 ⊼ (𝜒𝜓)) ⊼ ((𝜏 ⊼ (𝜏𝜏)) ⊼ ((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384  wnan 1608
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 198  df-an 385  df-nan 1609
This theorem is referenced by:  nic-imp  1770  nic-idlem1  1771  nic-idlem2  1772  nic-id  1773  nic-swap  1774  nic-luk1  1786  lukshef-ax1  1789
  Copyright terms: Public domain W3C validator