Theorem nic-axALT 1439

Description: A direct proof of nic-ax 1438. (Contributed by NM, 11-Dec-2008.) (Proof modification is discouraged.) (New usage is discouraged.)

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 443	. . . . . 6 |- ((ch /\ ps) -> ch)
2	1	imim2i 13	. . . . 5 |- ((ph -> (ch /\ ps)) -> (ph -> ch))
3		con3 126	. . . . . 6 |- ((ph -> ch) -> (-. ch -> -. ph))
4	3	imim2d 48	. . . . 5 |- ((ph -> ch) -> ((th -> -. ch) -> (th -> -. ph)))
5	2, 4	syl 15	. . . 4 |- ((ph -> (ch /\ ps)) -> ((th -> -. ch) -> (th -> -. ph)))
6		anidm 625	. . . . 5 |- ((ta /\ ta) <-> ta)
7	6	biimpri 197	. . . 4 |- (ta -> (ta /\ ta))
8	5, 7	jctil 523	. . 3 |- ((ph -> (ch /\ ps)) -> ((ta -> (ta /\ ta)) /\ ((th -> -. ch) -> (th -> -. ph))))
9		df-nan 1288	. . . . . . . . 9 |- ((ch -/\ ps) <-> -. (ch /\ ps))
10	9	anbi2i 675	. . . . . . . 8 |- ((ph /\ (ch -/\ ps)) <-> (ph /\ -. (ch /\ ps)))
11	10	notbii 287	. . . . . . 7 |- (-. (ph /\ (ch -/\ ps)) <-> -. (ph /\ -. (ch /\ ps)))
12		df-nan 1288	. . . . . . 7 |- ((ph -/\ (ch -/\ ps)) <-> -. (ph /\ (ch -/\ ps)))
13		iman 413	. . . . . . 7 |- ((ph -> (ch /\ ps)) <-> -. (ph /\ -. (ch /\ ps)))
14	11, 12, 13	3bitr4i 268	. . . . . 6 |- ((ph -/\ (ch -/\ ps)) <-> (ph -> (ch /\ ps)))
15		df-nan 1288	. . . . . . 7 |- (((ta -/\ (ta -/\ ta)) -/\ ((th -/\ ch) -/\ ((ph -/\ th) -/\ (ph -/\ th)))) <-> -. ((ta -/\ (ta -/\ ta)) /\ ((th -/\ ch) -/\ ((ph -/\ th) -/\ (ph -/\ th)))))
16		df-nan 1288	. . . . . . . . . . 11 |- ((ta -/\ ta) <-> -. (ta /\ ta))
17	16	anbi2i 675	. . . . . . . . . 10 |- ((ta /\ (ta -/\ ta)) <-> (ta /\ -. (ta /\ ta)))
18	17	notbii 287	. . . . . . . . 9 |- (-. (ta /\ (ta -/\ ta)) <-> -. (ta /\ -. (ta /\ ta)))
19		df-nan 1288	. . . . . . . . 9 |- ((ta -/\ (ta -/\ ta)) <-> -. (ta /\ (ta -/\ ta)))
20		iman 413	. . . . . . . . 9 |- ((ta -> (ta /\ ta)) <-> -. (ta /\ -. (ta /\ ta)))
21	18, 19, 20	3bitr4i 268	. . . . . . . 8 |- ((ta -/\ (ta -/\ ta)) <-> (ta -> (ta /\ ta)))
22		df-nan 1288	. . . . . . . . . . . 12 |- ((th -/\ ch) <-> -. (th /\ ch))
23		imnan 411	. . . . . . . . . . . 12 |- ((th -> -. ch) <-> -. (th /\ ch))
24	22, 23	bitr4i 243	. . . . . . . . . . 11 |- ((th -/\ ch) <-> (th -> -. ch))
25		df-nan 1288	. . . . . . . . . . . 12 |- (((ph -/\ th) -/\ (ph -/\ th)) <-> -. ((ph -/\ th) /\ (ph -/\ th)))
26		anidm 625	. . . . . . . . . . . . 13 |- (((ph -/\ th) /\ (ph -/\ th)) <-> (ph -/\ th))
27		df-nan 1288	. . . . . . . . . . . . 13 |- ((ph -/\ th) <-> -. (ph /\ th))
28		imnan 411	. . . . . . . . . . . . . 14 |- ((ph -> -. th) <-> -. (ph /\ th))
29		con2b 324	. . . . . . . . . . . . . 14 |- ((ph -> -. th) <-> (th -> -. ph))
30	28, 29	bitr3i 242	. . . . . . . . . . . . 13 |- (-. (ph /\ th) <-> (th -> -. ph))
31	26, 27, 30	3bitri 262	. . . . . . . . . . . 12 |- (((ph -/\ th) /\ (ph -/\ th)) <-> (th -> -. ph))
32	25, 31	xchbinx 301	. . . . . . . . . . 11 |- (((ph -/\ th) -/\ (ph -/\ th)) <-> -. (th -> -. ph))
33	24, 32	anbi12i 678	. . . . . . . . . 10 |- (((th -/\ ch) /\ ((ph -/\ th) -/\ (ph -/\ th))) <-> ((th -> -. ch) /\ -. (th -> -. ph)))
34	33	notbii 287	. . . . . . . . 9 |- (-. ((th -/\ ch) /\ ((ph -/\ th) -/\ (ph -/\ th))) <-> -. ((th -> -. ch) /\ -. (th -> -. ph)))
35		df-nan 1288	. . . . . . . . 9 |- (((th -/\ ch) -/\ ((ph -/\ th) -/\ (ph -/\ th))) <-> -. ((th -/\ ch) /\ ((ph -/\ th) -/\ (ph -/\ th))))
36		iman 413	. . . . . . . . 9 |- (((th -> -. ch) -> (th -> -. ph)) <-> -. ((th -> -. ch) /\ -. (th -> -. ph)))
37	34, 35, 36	3bitr4i 268	. . . . . . . 8 |- (((th -/\ ch) -/\ ((ph -/\ th) -/\ (ph -/\ th))) <-> ((th -> -. ch) -> (th -> -. ph)))
38	21, 37	anbi12i 678	. . . . . . 7 |- (((ta -/\ (ta -/\ ta)) /\ ((th -/\ ch) -/\ ((ph -/\ th) -/\ (ph -/\ th)))) <-> ((ta -> (ta /\ ta)) /\ ((th -> -. ch) -> (th -> -. ph))))
39	15, 38	xchbinx 301	. . . . . 6 |- (((ta -/\ (ta -/\ ta)) -/\ ((th -/\ ch) -/\ ((ph -/\ th) -/\ (ph -/\ th)))) <-> -. ((ta -> (ta /\ ta)) /\ ((th -> -. ch) -> (th -> -. ph))))
40	14, 39	anbi12i 678	. . . . 5 |- (((ph -/\ (ch -/\ ps)) /\ ((ta -/\ (ta -/\ ta)) -/\ ((th -/\ ch) -/\ ((ph -/\ th) -/\ (ph -/\ th))))) <-> ((ph -> (ch /\ ps)) /\ -. ((ta -> (ta /\ ta)) /\ ((th -> -. ch) -> (th -> -. ph)))))
41	40	notbii 287	. . . 4 |- (-. ((ph -/\ (ch -/\ ps)) /\ ((ta -/\ (ta -/\ ta)) -/\ ((th -/\ ch) -/\ ((ph -/\ th) -/\ (ph -/\ th))))) <-> -. ((ph -> (ch /\ ps)) /\ -. ((ta -> (ta /\ ta)) /\ ((th -> -. ch) -> (th -> -. ph)))))
42		iman 413	. . . 4 |- (((ph -> (ch /\ ps)) -> ((ta -> (ta /\ ta)) /\ ((th -> -. ch) -> (th -> -. ph)))) <-> -. ((ph -> (ch /\ ps)) /\ -. ((ta -> (ta /\ ta)) /\ ((th -> -. ch) -> (th -> -. ph)))))
43	41, 42	bitr4i 243	. . 3 |- (-. ((ph -/\ (ch -/\ ps)) /\ ((ta -/\ (ta -/\ ta)) -/\ ((th -/\ ch) -/\ ((ph -/\ th) -/\ (ph -/\ th))))) <-> ((ph -> (ch /\ ps)) -> ((ta -> (ta /\ ta)) /\ ((th -> -. ch) -> (th -> -. ph)))))
44	8, 43	mpbir 200	. 2 |- -. ((ph -/\ (ch -/\ ps)) /\ ((ta -/\ (ta -/\ ta)) -/\ ((th -/\ ch) -/\ ((ph -/\ th) -/\ (ph -/\ th)))))
45		df-nan 1288	. 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))))))
46	44, 45	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: (None)