Theorem nicodraw 950

Description: Axiom of Nicod from Introduction to Mathematical Philosophy B. Russell, p. 152. The axiom is recovered from this raw form by substituting (ph | ps) for -. (ph /\ ps), where | is the Sheffer stroke (NAND) connective, so that the Sheffer stroke becomes the sole connective. See nicodmpraw 951 for the inference rule. (Based on a proof by Jeff Hoffman, 19-Nov-2007.)

Assertion

Ref	Expression
nicodraw	|- -. (-. (ph /\ -. (ch /\ ps)) /\ -. (-. (ta /\ -. (ta /\ ta)) /\ -. (-. (th /\ ch) /\ -. (-. (ph /\ th) /\ -. (ph /\ th)))))

Proof of Theorem nicodraw

Step	Hyp	Ref	Expression
1		iman 237	. . . . 5 |- ((ph -> (ch /\ ps)) <-> -. (ph /\ -. (ch /\ ps)))
2	1	biimpr 152	. . . 4 |- (-. (ph /\ -. (ch /\ ps)) -> (ph -> (ch /\ ps)))
3		pm3.26 319	. . . . 5 |- ((ch /\ ps) -> ch)
4	3	imim2i 17	. . . 4 |- ((ph -> (ch /\ ps)) -> (ph -> ch))
5		con3 94	. . . . . . . 8 |- ((ph -> ch) -> (-. ch -> -. ph))
6	5	imim2d 25	. . . . . . 7 |- ((ph -> ch) -> ((th -> -. ch) -> (th -> -. ph)))
7		bi2.03 165	. . . . . . . 8 |- ((th -> -. ph) <-> (ph -> -. th))
8		imnan 242	. . . . . . . 8 |- ((ph -> -. th) <-> -. (ph /\ th))
9	7, 8	bitr2 174	. . . . . . 7 |- (-. (ph /\ th) <-> (th -> -. ph))
10	6, 9	syl6ibr 213	. . . . . 6 |- ((ph -> ch) -> ((th -> -. ch) -> -. (ph /\ th)))
11		imnan 242	. . . . . 6 |- ((th -> -. ch) <-> -. (th /\ ch))
12	10, 11	syl5ibr 207	. . . . 5 |- ((ph -> ch) -> (-. (th /\ ch) -> -. (ph /\ th)))
13		iman 237	. . . . . 6 |- ((-. (th /\ ch) -> (-. (ph /\ th) /\ -. (ph /\ th))) <-> -. (-. (th /\ ch) /\ -. (-. (ph /\ th) /\ -. (ph /\ th))))
14		anidm 432	. . . . . . 7 |- ((-. (ph /\ th) /\ -. (ph /\ th)) <-> -. (ph /\ th))
15	14	imbi2i 185	. . . . . 6 |- ((-. (th /\ ch) -> (-. (ph /\ th) /\ -. (ph /\ th))) <-> (-. (th /\ ch) -> -. (ph /\ th)))
16	13, 15	bitr3 175	. . . . 5 |- (-. (-. (th /\ ch) /\ -. (-. (ph /\ th) /\ -. (ph /\ th))) <-> (-. (th /\ ch) -> -. (ph /\ th)))
17	12, 16	sylibr 200	. . . 4 |- ((ph -> ch) -> -. (-. (th /\ ch) /\ -. (-. (ph /\ th) /\ -. (ph /\ th))))
18	2, 4, 17	3syl 20	. . 3 |- (-. (ph /\ -. (ch /\ ps)) -> -. (-. (th /\ ch) /\ -. (-. (ph /\ th) /\ -. (ph /\ th))))
19		pm4.24 433	. . . . 5 |- (ta <-> (ta /\ ta))
20	19	biimp 151	. . . 4 |- (ta -> (ta /\ ta))
21		iman 237	. . . 4 |- ((ta -> (ta /\ ta)) <-> -. (ta /\ -. (ta /\ ta)))
22	20, 21	mpbi 189	. . 3 |- -. (ta /\ -. (ta /\ ta))
23	18, 22	jctil 292	. 2 |- (-. (ph /\ -. (ch /\ ps)) -> (-. (ta /\ -. (ta /\ ta)) /\ -. (-. (th /\ ch) /\ -. (-. (ph /\ th) /\ -. (ph /\ th)))))
24		iman 237	. 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	mpbi 189	1 |- -. (-. (ph /\ -. (ch /\ ps)) /\ -. (-. (ta /\ -. (ta /\ ta)) /\ -. (-. (th /\ ch) /\ -. (-. (ph /\ th) /\ -. (ph /\ th)))))

Syntax hints:  -. wn 2   -> wi 3   /\ wa 223

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain