Theorem nic-axALT 1240

Description: A direct proof of nic-ax 1239.

Assertion

Ref	Expression
nic-axALT	|- ((ph -/\ (ch -/\ ps)) -/\ ((ta -/\ (ta -/\ ta)) -/\ ((th -/\ ch) -/\ ((ph -/\ th) -/\ (ph -/\ th)))))

Proof of Theorem nic-axALT

Step	Hyp	Ref	Expression
1		simpl 346	. . . . . 6 |- ((ch /\ ps) -> ch)
2	1	imim2i 11	. . . . 5 |- ((ph -> (ch /\ ps)) -> (ph -> ch))
3		con3 110	. . . . . 6 |- ((ph -> ch) -> (-. ch -> -. ph))
4	3	imim2d 28	. . . . 5 |- ((ph -> ch) -> ((th -> -. ch) -> (th -> -. ph)))
5	2, 4	syl 12	. . . 4 |- ((ph -> (ch /\ ps)) -> ((th -> -. ch) -> (th -> -. ph)))
6		anidm 478	. . . . 5 |- ((ta /\ ta) <-> ta)
7	6	biimpri 169	. . . 4 |- (ta -> (ta /\ ta))
8	5, 7	jctil 316	. . 3 |- ((ph -> (ch /\ ps)) -> ((ta -> (ta /\ ta)) /\ ((th -> -. ch) -> (th -> -. ph))))
9		df-nand 1230	. . . . . . . . 9 |- ((ch -/\ ps) <-> -. (ch /\ ps))
10	9	anbi2i 538	. . . . . . . 8 |- ((ph /\ (ch -/\ ps)) <-> (ph /\ -. (ch /\ ps)))
11	10	notbii 204	. . . . . . 7 |- (-. (ph /\ (ch -/\ ps)) <-> -. (ph /\ -. (ch /\ ps)))
12		df-nand 1230	. . . . . . 7 |- ((ph -/\ (ch -/\ ps)) <-> -. (ph /\ (ch -/\ ps)))
13		iman 256	. . . . . . 7 |- ((ph -> (ch /\ ps)) <-> -. (ph /\ -. (ch /\ ps)))
14	11, 12, 13	3bitr4i 200	. . . . . 6 |- ((ph -/\ (ch -/\ ps)) <-> (ph -> (ch /\ ps)))
15		df-nand 1230	. . . . . . 7 |- (((ta -/\ (ta -/\ ta)) -/\ ((th -/\ ch) -/\ ((ph -/\ th) -/\ (ph -/\ th)))) <-> -. ((ta -/\ (ta -/\ ta)) /\ ((th -/\ ch) -/\ ((ph -/\ th) -/\ (ph -/\ th)))))
16		df-nand 1230	. . . . . . . . . . . 12 |- ((ta -/\ ta) <-> -. (ta /\ ta))
17	16	anbi2i 538	. . . . . . . . . . 11 |- ((ta /\ (ta -/\ ta)) <-> (ta /\ -. (ta /\ ta)))
18	17	notbii 204	. . . . . . . . . 10 |- (-. (ta /\ (ta -/\ ta)) <-> -. (ta /\ -. (ta /\ ta)))
19		df-nand 1230	. . . . . . . . . 10 |- ((ta -/\ (ta -/\ ta)) <-> -. (ta /\ (ta -/\ ta)))
20		iman 256	. . . . . . . . . 10 |- ((ta -> (ta /\ ta)) <-> -. (ta /\ -. (ta /\ ta)))
21	18, 19, 20	3bitr4i 200	. . . . . . . . 9 |- ((ta -/\ (ta -/\ ta)) <-> (ta -> (ta /\ ta)))
22		df-nand 1230	. . . . . . . . . . . . 13 |- ((th -/\ ch) <-> -. (th /\ ch))
23		imnan 261	. . . . . . . . . . . . 13 |- ((th -> -. ch) <-> -. (th /\ ch))
24	22, 23	bitr4i 193	. . . . . . . . . . . 12 |- ((th -/\ ch) <-> (th -> -. ch))
25		df-nand 1230	. . . . . . . . . . . . 13 |- (((ph -/\ th) -/\ (ph -/\ th)) <-> -. ((ph -/\ th) /\ (ph -/\ th)))
26		anidm 478	. . . . . . . . . . . . . . 15 |- (((ph -/\ th) /\ (ph -/\ th)) <-> (ph -/\ th))
27		df-nand 1230	. . . . . . . . . . . . . . 15 |- ((ph -/\ th) <-> -. (ph /\ th))
28		imnan 261	. . . . . . . . . . . . . . . 16 |- ((ph -> -. th) <-> -. (ph /\ th))
29		con2b 182	. . . . . . . . . . . . . . . 16 |- ((ph -> -. th) <-> (th -> -. ph))
30	28, 29	bitr3i 192	. . . . . . . . . . . . . . 15 |- (-. (ph /\ th) <-> (th -> -. ph))
31	26, 27, 30	3bitri 194	. . . . . . . . . . . . . 14 |- (((ph -/\ th) /\ (ph -/\ th)) <-> (th -> -. ph))
32	31	notbii 204	. . . . . . . . . . . . 13 |- (-. ((ph -/\ th) /\ (ph -/\ th)) <-> -. (th -> -. ph))
33	25, 32	bitri 190	. . . . . . . . . . . 12 |- (((ph -/\ th) -/\ (ph -/\ th)) <-> -. (th -> -. ph))
34	24, 33	anbi12i 540	. . . . . . . . . . 11 |- (((th -/\ ch) /\ ((ph -/\ th) -/\ (ph -/\ th))) <-> ((th -> -. ch) /\ -. (th -> -. ph)))
35	34	notbii 204	. . . . . . . . . 10 |- (-. ((th -/\ ch) /\ ((ph -/\ th) -/\ (ph -/\ th))) <-> -. ((th -> -. ch) /\ -. (th -> -. ph)))
36		df-nand 1230	. . . . . . . . . 10 |- (((th -/\ ch) -/\ ((ph -/\ th) -/\ (ph -/\ th))) <-> -. ((th -/\ ch) /\ ((ph -/\ th) -/\ (ph -/\ th))))
37		iman 256	. . . . . . . . . 10 |- (((th -> -. ch) -> (th -> -. ph)) <-> -. ((th -> -. ch) /\ -. (th -> -. ph)))
38	35, 36, 37	3bitr4i 200	. . . . . . . . 9 |- (((th -/\ ch) -/\ ((ph -/\ th) -/\ (ph -/\ th))) <-> ((th -> -. ch) -> (th -> -. ph)))
39	21, 38	anbi12i 540	. . . . . . . 8 |- (((ta -/\ (ta -/\ ta)) /\ ((th -/\ ch) -/\ ((ph -/\ th) -/\ (ph -/\ th)))) <-> ((ta -> (ta /\ ta)) /\ ((th -> -. ch) -> (th -> -. ph))))
40	39	notbii 204	. . . . . . 7 |- (-. ((ta -/\ (ta -/\ ta)) /\ ((th -/\ ch) -/\ ((ph -/\ th) -/\ (ph -/\ th)))) <-> -. ((ta -> (ta /\ ta)) /\ ((th -> -. ch) -> (th -> -. ph))))
41	15, 40	bitri 190	. . . . . 6 |- (((ta -/\ (ta -/\ ta)) -/\ ((th -/\ ch) -/\ ((ph -/\ th) -/\ (ph -/\ th)))) <-> -. ((ta -> (ta /\ ta)) /\ ((th -> -. ch) -> (th -> -. ph))))
42	14, 41	anbi12i 540	. . . . 5 |- (((ph -/\ (ch -/\ ps)) /\ ((ta -/\ (ta -/\ ta)) -/\ ((th -/\ ch) -/\ ((ph -/\ th) -/\ (ph -/\ th))))) <-> ((ph -> (ch /\ ps)) /\ -. ((ta -> (ta /\ ta)) /\ ((th -> -. ch) -> (th -> -. ph)))))
43	42	notbii 204	. . . 4 |- (-. ((ph -/\ (ch -/\ ps)) /\ ((ta -/\ (ta -/\ ta)) -/\ ((th -/\ ch) -/\ ((ph -/\ th) -/\ (ph -/\ th))))) <-> -. ((ph -> (ch /\ ps)) /\ -. ((ta -> (ta /\ ta)) /\ ((th -> -. ch) -> (th -> -. ph)))))
44		iman 256	. . . 4 |- (((ph -> (ch /\ ps)) -> ((ta -> (ta /\ ta)) /\ ((th -> -. ch) -> (th -> -. ph)))) <-> -. ((ph -> (ch /\ ps)) /\ -. ((ta -> (ta /\ ta)) /\ ((th -> -. ch) -> (th -> -. ph)))))
45	43, 44	bitr4i 193	. . 3 |- (-. ((ph -/\ (ch -/\ ps)) /\ ((ta -/\ (ta -/\ ta)) -/\ ((th -/\ ch) -/\ ((ph -/\ th) -/\ (ph -/\ th))))) <-> ((ph -> (ch /\ ps)) -> ((ta -> (ta /\ ta)) /\ ((th -> -. ch) -> (th -> -. ph)))))
46	8, 45	mpbir 207	. 2 |- -. ((ph -/\ (ch -/\ ps)) /\ ((ta -/\ (ta -/\ ta)) -/\ ((th -/\ ch) -/\ ((ph -/\ th) -/\ (ph -/\ th)))))
47		df-nand 1230	. 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))))))
48	46, 47	mpbir 207	1 |- ((ph -/\ (ch -/\ ps)) -/\ ((ta -/\ (ta -/\ ta)) -/\ ((th -/\ ch) -/\ ((ph -/\ th) -/\ (ph -/\ th)))))

Syntax hints:  -. wn 2   -> wi 3   /\ wa 240   -/\ wnand 1229

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 164  df-an 242  df-nand 1230

Copyright terms: Public domain