Theorem nic-ax 1598

Description: Nicod's axiom derived from the standard ones. See Introduction to Mathematical Philosophy by B. Russell, p. 152. Like meredith 1566, the usual axioms can be derived from this and vice versa. Unlike meredith 1566, Nicod uses a different connective ('nand'), so another form of modus ponens must be used in proofs, e.g. { nic-ax 1598, nic-mp 1596 } is equivalent to { luk-1 1580, luk-2 1581, luk-3 1582, 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	|- ( ( ph -/\ ( ch -/\ ps ) ) -/\ ( ( ta -/\ ( ta -/\ ta ) ) -/\ ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) ) )

Proof of Theorem nic-ax

Step	Hyp	Ref	Expression
1		nannan 1451	. . . . 5 |- ( ( ph -/\ ( ch -/\ ps ) ) <-> ( ph -> ( ch /\ ps ) ) )
2	1	biimpi 206	. . . 4 |- ( ( ph -/\ ( ch -/\ ps ) ) -> ( ph -> ( ch /\ ps ) ) )
3		simpl 473	. . . . 5 |- ( ( ch /\ ps ) -> ch )
4	3	imim2i 16	. . . 4 |- ( ( ph -> ( ch /\ ps ) ) -> ( ph -> ch ) )
5		imnan 438	. . . . . . 7 |- ( ( th -> -. ch ) <-> -. ( th /\ ch ) )
6		df-nan 1448	. . . . . . 7 |- ( ( th -/\ ch ) <-> -. ( th /\ ch ) )
7	5, 6	bitr4i 267	. . . . . 6 |- ( ( th -> -. ch ) <-> ( th -/\ ch ) )
8		con3 149	. . . . . . . 8 |- ( ( ph -> ch ) -> ( -. ch -> -. ph ) )
9	8	imim2d 57	. . . . . . 7 |- ( ( ph -> ch ) -> ( ( th -> -. ch ) -> ( th -> -. ph ) ) )
10		imnan 438	. . . . . . . 8 |- ( ( ph -> -. th ) <-> -. ( ph /\ th ) )
11		con2b 349	. . . . . . . 8 |- ( ( th -> -. ph ) <-> ( ph -> -. th ) )
12		df-nan 1448	. . . . . . . 8 |- ( ( ph -/\ th ) <-> -. ( ph /\ th ) )
13	10, 11, 12	3bitr4ri 293	. . . . . . 7 |- ( ( ph -/\ th ) <-> ( th -> -. ph ) )
14	9, 13	syl6ibr 242	. . . . . 6 |- ( ( ph -> ch ) -> ( ( th -> -. ch ) -> ( ph -/\ th ) ) )
15	7, 14	syl5bir 233	. . . . 5 |- ( ( ph -> ch ) -> ( ( th -/\ ch ) -> ( ph -/\ th ) ) )
16		nanim 1452	. . . . 5 |- ( ( ( th -/\ ch ) -> ( ph -/\ th ) ) <-> ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) )
17	15, 16	sylib 208	. . . 4 |- ( ( ph -> ch ) -> ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) )
18	2, 4, 17	3syl 18	. . 3 |- ( ( ph -/\ ( ch -/\ ps ) ) -> ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) )
19		pm4.24 675	. . . . 5 |- ( ta <-> ( ta /\ ta ) )
20	19	biimpi 206	. . . 4 |- ( ta -> ( ta /\ ta ) )
21		nannan 1451	. . . 4 |- ( ( ta -/\ ( ta -/\ ta ) ) <-> ( ta -> ( ta /\ ta ) ) )
22	20, 21	mpbir 221	. . 3 |- ( ta -/\ ( ta -/\ ta ) )
23	18, 22	jctil 560	. 2 |- ( ( ph -/\ ( ch -/\ ps ) ) -> ( ( ta -/\ ( ta -/\ ta ) ) /\ ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) ) )
24		nannan 1451	. 2 |- ( ( ( ph -/\ ( ch -/\ ps ) ) -/\ ( ( ta -/\ ( ta -/\ ta ) ) -/\ ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) ) ) <-> ( ( ph -/\ ( ch -/\ ps ) ) -> ( ( ta -/\ ( ta -/\ ta ) ) /\ ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) ) ) )
25	23, 24	mpbir 221	1 |- ( ( ph -/\ ( ch -/\ ps ) ) -/\ ( ( ta -/\ ( ta -/\ ta ) ) -/\ ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 384   -/\ wnan 1447

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 197  df-an 386  df-nan 1448

This theorem is referenced by:  nic-imp  1600  nic-idlem1  1601  nic-idlem2  1602  nic-id  1603  nic-swap  1604  nic-luk1  1616  lukshef-ax1  1619