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 1667
Description: Nicod's axiom derived from the standard ones. See Introduction to Mathematical Philosophy by B. Russell, p. 152. Like meredith 1635, the usual axioms can be derived from this and vice versa. Unlike meredith 1635, Nicod uses a different connective ('nand'), so another form of modus ponens must be used in proofs, e.g., { nic-ax 1667, nic-mp 1665 } is equivalent to { luk-1 1649, luk-2 1650, luk-3 1651, 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 1490 . . . . 5 ((𝜑 ⊼ (𝜒𝜓)) ↔ (𝜑 → (𝜒𝜓)))
21biimpi 215 . . . 4 ((𝜑 ⊼ (𝜒𝜓)) → (𝜑 → (𝜒𝜓)))
3 simpl 482 . . . . 5 ((𝜒𝜓) → 𝜒)
43imim2i 16 . . . 4 ((𝜑 → (𝜒𝜓)) → (𝜑𝜒))
5 imnan 399 . . . . . . 7 ((𝜃 → ¬ 𝜒) ↔ ¬ (𝜃𝜒))
6 df-nan 1485 . . . . . . 7 ((𝜃𝜒) ↔ ¬ (𝜃𝜒))
75, 6bitr4i 278 . . . . . 6 ((𝜃 → ¬ 𝜒) ↔ (𝜃𝜒))
8 con3 153 . . . . . . . 8 ((𝜑𝜒) → (¬ 𝜒 → ¬ 𝜑))
98imim2d 57 . . . . . . 7 ((𝜑𝜒) → ((𝜃 → ¬ 𝜒) → (𝜃 → ¬ 𝜑)))
10 imnan 399 . . . . . . . 8 ((𝜑 → ¬ 𝜃) ↔ ¬ (𝜑𝜃))
11 con2b 359 . . . . . . . 8 ((𝜃 → ¬ 𝜑) ↔ (𝜑 → ¬ 𝜃))
12 df-nan 1485 . . . . . . . 8 ((𝜑𝜃) ↔ ¬ (𝜑𝜃))
1310, 11, 123bitr4ri 304 . . . . . . 7 ((𝜑𝜃) ↔ (𝜃 → ¬ 𝜑))
149, 13imbitrrdi 251 . . . . . 6 ((𝜑𝜒) → ((𝜃 → ¬ 𝜒) → (𝜑𝜃)))
157, 14biimtrrid 242 . . . . 5 ((𝜑𝜒) → ((𝜃𝜒) → (𝜑𝜃)))
16 nanim 1491 . . . . 5 (((𝜃𝜒) → (𝜑𝜃)) ↔ ((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃))))
1715, 16sylib 217 . . . 4 ((𝜑𝜒) → ((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃))))
182, 4, 173syl 18 . . 3 ((𝜑 ⊼ (𝜒𝜓)) → ((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃))))
19 pm4.24 563 . . . . 5 (𝜏 ↔ (𝜏𝜏))
2019biimpi 215 . . . 4 (𝜏 → (𝜏𝜏))
21 nannan 1490 . . . 4 ((𝜏 ⊼ (𝜏𝜏)) ↔ (𝜏 → (𝜏𝜏)))
2220, 21mpbir 230 . . 3 (𝜏 ⊼ (𝜏𝜏))
2318, 22jctil 519 . 2 ((𝜑 ⊼ (𝜒𝜓)) → ((𝜏 ⊼ (𝜏𝜏)) ∧ ((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃)))))
24 nannan 1490 . 2 (((𝜑 ⊼ (𝜒𝜓)) ⊼ ((𝜏 ⊼ (𝜏𝜏)) ⊼ ((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃))))) ↔ ((𝜑 ⊼ (𝜒𝜓)) → ((𝜏 ⊼ (𝜏𝜏)) ∧ ((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃))))))
2523, 24mpbir 230 1 ((𝜑 ⊼ (𝜒𝜓)) ⊼ ((𝜏 ⊼ (𝜏𝜏)) ⊼ ((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  wnan 1484
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 1485
This theorem is referenced by:  nic-imp  1669  nic-idlem1  1670  nic-idlem2  1671  nic-id  1672  nic-swap  1673  nic-luk1  1685  lukshef-ax1  1688
  Copyright terms: Public domain W3C validator