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	|- ((ph -/\ (ch -/\ ps)) -/\ ((ta -/\ (ta -/\ ta)) -/\ ((th -/\ ch) -/\ ((ph -/\ th) -/\ (ph -/\ th)))))

Proof of Theorem nic-ax

Step	Hyp	Ref	Expression
1		nannan 1291	. . . . 5 |- ((ph -/\ (ch -/\ ps)) <-> (ph -> (ch /\ ps)))
2	1	biimpi 186	. . . 4 |- ((ph -/\ (ch -/\ ps)) -> (ph -> (ch /\ ps)))
3		simpl 443	. . . . 5 |- ((ch /\ ps) -> ch)
4	3	imim2i 13	. . . 4 |- ((ph -> (ch /\ ps)) -> (ph -> ch))
5		imnan 411	. . . . . . 7 |- ((th -> -. ch) <-> -. (th /\ ch))
6		df-nan 1288	. . . . . . 7 |- ((th -/\ ch) <-> -. (th /\ ch))
7	5, 6	bitr4i 243	. . . . . 6 |- ((th -> -. ch) <-> (th -/\ ch))
8		con3 126	. . . . . . . 8 |- ((ph -> ch) -> (-. ch -> -. ph))
9	8	imim2d 48	. . . . . . 7 |- ((ph -> ch) -> ((th -> -. ch) -> (th -> -. ph)))
10		imnan 411	. . . . . . . 8 |- ((ph -> -. th) <-> -. (ph /\ th))
11		con2b 324	. . . . . . . 8 |- ((th -> -. ph) <-> (ph -> -. th))
12		df-nan 1288	. . . . . . . 8 |- ((ph -/\ th) <-> -. (ph /\ th))
13	10, 11, 12	3bitr4ri 269	. . . . . . 7 |- ((ph -/\ th) <-> (th -> -. ph))
14	9, 13	syl6ibr 218	. . . . . 6 |- ((ph -> ch) -> ((th -> -. ch) -> (ph -/\ th)))
15	7, 14	syl5bir 209	. . . . 5 |- ((ph -> ch) -> ((th -/\ ch) -> (ph -/\ th)))
16		nanim 1292	. . . . 5 |- (((th -/\ ch) -> (ph -/\ th)) <-> ((th -/\ ch) -/\ ((ph -/\ th) -/\ (ph -/\ th))))
17	15, 16	sylib 188	. . . 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 624	. . . . 5 |- (ta <-> (ta /\ ta))
20	19	biimpi 186	. . . 4 |- (ta -> (ta /\ ta))
21		nannan 1291	. . . 4 |- ((ta -/\ (ta -/\ ta)) <-> (ta -> (ta /\ ta)))
22	20, 21	mpbir 200	. . 3 |- (ta -/\ (ta -/\ ta))
23	18, 22	jctil 523	. 2 |- ((ph -/\ (ch -/\ ps)) -> ((ta -/\ (ta -/\ ta)) /\ ((th -/\ ch) -/\ ((ph -/\ th) -/\ (ph -/\ th)))))
24		nannan 1291	. 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 200	1 |- ((ph -/\ (ch -/\ ps)) -/\ ((ta -/\ (ta -/\ ta)) -/\ ((th -/\ ch) -/\ ((ph -/\ th) -/\ (ph -/\ th)))))

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