New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > nic-ax | Unicode version |
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 8 . 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.) |
Ref | Expression |
---|---|
nic-ax |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nannan 1291 | . . . . 5 | |
2 | 1 | biimpi 186 | . . . 4 |
3 | simpl 443 | . . . . 5 | |
4 | 3 | imim2i 13 | . . . 4 |
5 | imnan 411 | . . . . . . 7 | |
6 | df-nan 1288 | . . . . . . 7 | |
7 | 5, 6 | bitr4i 243 | . . . . . 6 |
8 | con3 126 | . . . . . . . 8 | |
9 | 8 | imim2d 48 | . . . . . . 7 |
10 | imnan 411 | . . . . . . . 8 | |
11 | con2b 324 | . . . . . . . 8 | |
12 | df-nan 1288 | . . . . . . . 8 | |
13 | 10, 11, 12 | 3bitr4ri 269 | . . . . . . 7 |
14 | 9, 13 | syl6ibr 218 | . . . . . 6 |
15 | 7, 14 | syl5bir 209 | . . . . 5 |
16 | nanim 1292 | . . . . 5 | |
17 | 15, 16 | sylib 188 | . . . 4 |
18 | 2, 4, 17 | 3syl 18 | . . 3 |
19 | pm4.24 624 | . . . . 5 | |
20 | 19 | biimpi 186 | . . . 4 |
21 | nannan 1291 | . . . 4 | |
22 | 20, 21 | mpbir 200 | . . 3 |
23 | 18, 22 | jctil 523 | . 2 |
24 | nannan 1291 | . 2 | |
25 | 23, 24 | mpbir 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-1 5 ax-2 6 ax-3 7 ax-mp 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 |