NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  nic-ax GIF version

Theorem nic-ax 1438
Description: Nicod's axiom derived from the standard ones. See Intro. to Math. Phil. by B. Russell, p. 152. Like meredith 1404, the usual axioms can be derived from this and vice versa. Unlike meredith 1404, Nicod uses a different connective ('nand'), so another form of modus ponens must be used in proofs, e.g. { nic-ax 1438, nic-mp 1436 } is equivalent to { luk-1 1420, luk-2 1421, luk-3 1422, 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 1291 . . . . 5 ((φ (χ ψ)) ↔ (φ → (χ ψ)))
21biimpi 186 . . . 4 ((φ (χ ψ)) → (φ → (χ ψ)))
3 simpl 443 . . . . 5 ((χ ψ) → χ)
43imim2i 13 . . . 4 ((φ → (χ ψ)) → (φχ))
5 imnan 411 . . . . . . 7 ((θ → ¬ χ) ↔ ¬ (θ χ))
6 df-nan 1288 . . . . . . 7 ((θ χ) ↔ ¬ (θ χ))
75, 6bitr4i 243 . . . . . 6 ((θ → ¬ χ) ↔ (θ χ))
8 con3 126 . . . . . . . 8 ((φχ) → (¬ χ → ¬ φ))
98imim2d 48 . . . . . . 7 ((φχ) → ((θ → ¬ χ) → (θ → ¬ φ)))
10 imnan 411 . . . . . . . 8 ((φ → ¬ θ) ↔ ¬ (φ θ))
11 con2b 324 . . . . . . . 8 ((θ → ¬ φ) ↔ (φ → ¬ θ))
12 df-nan 1288 . . . . . . . 8 ((φ θ) ↔ ¬ (φ θ))
1310, 11, 123bitr4ri 269 . . . . . . 7 ((φ θ) ↔ (θ → ¬ φ))
149, 13syl6ibr 218 . . . . . 6 ((φχ) → ((θ → ¬ χ) → (φ θ)))
157, 14syl5bir 209 . . . . 5 ((φχ) → ((θ χ) → (φ θ)))
16 nanim 1292 . . . . 5 (((θ χ) → (φ θ)) ↔ ((θ χ) ((φ θ) (φ θ))))
1715, 16sylib 188 . . . 4 ((φχ) → ((θ χ) ((φ θ) (φ θ))))
182, 4, 173syl 18 . . 3 ((φ (χ ψ)) → ((θ χ) ((φ θ) (φ θ))))
19 pm4.24 624 . . . . 5 (τ ↔ (τ τ))
2019biimpi 186 . . . 4 (τ → (τ τ))
21 nannan 1291 . . . 4 ((τ (τ τ)) ↔ (τ → (τ τ)))
2220, 21mpbir 200 . . 3 (τ (τ τ))
2318, 22jctil 523 . 2 ((φ (χ ψ)) → ((τ (τ τ)) ((θ χ) ((φ θ) (φ θ)))))
24 nannan 1291 . 2 (((φ (χ ψ)) ((τ (τ τ)) ((θ χ) ((φ θ) (φ θ))))) ↔ ((φ (χ ψ)) → ((τ (τ τ)) ((θ χ) ((φ θ) (φ θ))))))
2523, 24mpbir 200 1 ((φ (χ ψ)) ((τ (τ τ)) ((θ χ) ((φ θ) (φ θ)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   wa 358   wnan 1287
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 177  df-an 360  df-nan 1288
This theorem is referenced by:  nic-imp  1440  nic-idlem1  1441  nic-idlem2  1442  nic-id  1443  nic-swap  1444  nic-luk1  1456  lukshef-ax1  1459
  Copyright terms: Public domain W3C validator