Theorem nic-ax 1506

Description: Nicod's axiom derived from the standard ones. See Introduction to Mathematical Philosophy by B. Russell, p. 152. Like meredith 1472, the usual axioms can be derived from this and vice versa. Unlike meredith 1472, Nicod uses a different connective ('nand'), so another form of modus ponens must be used in proofs, e.g. { nic-ax 1506, nic-mp 1504 } is equivalent to { luk-1 1488, luk-2 1489, luk-3 1490, 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

Step	Hyp	Ref	Expression
1		nannan 1348	. . . . 5
2	1	biimpi 194	. . . 4
3		simpl 457	. . . . 5
4	3	imim2i 14	. . . 4
5		imnan 422	. . . . . . 7
6		df-nan 1344	. . . . . . 7
7	5, 6	bitr4i 252	. . . . . 6
8		con3 134	. . . . . . . 8
9	8	imim2d 52	. . . . . . 7
10		imnan 422	. . . . . . . 8
11		con2b 334	. . . . . . . 8
12		df-nan 1344	. . . . . . . 8
13	10, 11, 12	3bitr4ri 278	. . . . . . 7
14	9, 13	syl6ibr 227	. . . . . 6
15	7, 14	syl5bir 218	. . . . 5
16		nanim 1350	. . . . 5
17	15, 16	sylib 196	. . . 4
18	2, 4, 17	3syl 20	. . 3
19		pm4.24 643	. . . . 5
20	19	biimpi 194	. . . 4
21		nannan 1348	. . . 4
22	20, 21	mpbir 209	. . 3
23	18, 22	jctil 537	. 2
24		nannan 1348	. 2
25	23, 24	mpbir 209	1

Syntax hints:  -.wn 3  ->wi 4  /\wa 369  -/\wnan 1343

This theorem is referenced by:  nic-imp  1508  nic-idlem1  1509  nic-idlem2  1510  nic-id  1511  nic-swap  1512  nic-luk1  1524  lukshef-ax1  1527

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 185  df-an 371  df-nan 1344