Theorem nic-axALT 1557

Description: A direct proof of nic-ax 1556. (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 459	. . . . . 6 |- ( ( ch /\ ps ) -> ch )
2	1	imim2i 16	. . . . 5 |- ( ( ph -> ( ch /\ ps ) ) -> ( ph -> ch ) )
3		con3 140	. . . . . 6 |- ( ( ph -> ch ) -> ( -. ch -> -. ph ) )
4	3	imim2d 54	. . . . 5 |- ( ( ph -> ch ) -> ( ( th -> -. ch ) -> ( th -> -. ph ) ) )
5	2, 4	syl 17	. . . 4 |- ( ( ph -> ( ch /\ ps ) ) -> ( ( th -> -. ch ) -> ( th -> -. ph ) ) )
6		anidm 650	. . . . 5 |- ( ( ta /\ ta ) <-> ta )
7	6	biimpri 210	. . . 4 |- ( ta -> ( ta /\ ta ) )
8	5, 7	jctil 540	. . 3 |- ( ( ph -> ( ch /\ ps ) ) -> ( ( ta -> ( ta /\ ta ) ) /\ ( ( th -> -. ch ) -> ( th -> -. ph ) ) ) )
9		df-nan 1385	. . . . . . . . 9 |- ( ( ch -/\ ps ) <-> -. ( ch /\ ps ) )
10	9	anbi2i 700	. . . . . . . 8 |- ( ( ph /\ ( ch -/\ ps ) ) <-> ( ph /\ -. ( ch /\ ps ) ) )
11	10	notbii 298	. . . . . . 7 |- ( -. ( ph /\ ( ch -/\ ps ) ) <-> -. ( ph /\ -. ( ch /\ ps ) ) )
12		df-nan 1385	. . . . . . 7 |- ( ( ph -/\ ( ch -/\ ps ) ) <-> -. ( ph /\ ( ch -/\ ps ) ) )
13		iman 426	. . . . . . 7 |- ( ( ph -> ( ch /\ ps ) ) <-> -. ( ph /\ -. ( ch /\ ps ) ) )
14	11, 12, 13	3bitr4i 281	. . . . . 6 |- ( ( ph -/\ ( ch -/\ ps ) ) <-> ( ph -> ( ch /\ ps ) ) )
15		df-nan 1385	. . . . . . 7 |- ( ( ( ta -/\ ( ta -/\ ta ) ) -/\ ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) ) <-> -. ( ( ta -/\ ( ta -/\ ta ) ) /\ ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) ) )
16		df-nan 1385	. . . . . . . . . . 11 |- ( ( ta -/\ ta ) <-> -. ( ta /\ ta ) )
17	16	anbi2i 700	. . . . . . . . . 10 |- ( ( ta /\ ( ta -/\ ta ) ) <-> ( ta /\ -. ( ta /\ ta ) ) )
18	17	notbii 298	. . . . . . . . 9 |- ( -. ( ta /\ ( ta -/\ ta ) ) <-> -. ( ta /\ -. ( ta /\ ta ) ) )
19		df-nan 1385	. . . . . . . . 9 |- ( ( ta -/\ ( ta -/\ ta ) ) <-> -. ( ta /\ ( ta -/\ ta ) ) )
20		iman 426	. . . . . . . . 9 |- ( ( ta -> ( ta /\ ta ) ) <-> -. ( ta /\ -. ( ta /\ ta ) ) )
21	18, 19, 20	3bitr4i 281	. . . . . . . 8 |- ( ( ta -/\ ( ta -/\ ta ) ) <-> ( ta -> ( ta /\ ta ) ) )
22		df-nan 1385	. . . . . . . . . . . 12 |- ( ( th -/\ ch ) <-> -. ( th /\ ch ) )
23		imnan 424	. . . . . . . . . . . 12 |- ( ( th -> -. ch ) <-> -. ( th /\ ch ) )
24	22, 23	bitr4i 256	. . . . . . . . . . 11 |- ( ( th -/\ ch ) <-> ( th -> -. ch ) )
25		df-nan 1385	. . . . . . . . . . . 12 |- ( ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) <-> -. ( ( ph -/\ th ) /\ ( ph -/\ th ) ) )
26		anidm 650	. . . . . . . . . . . . 13 |- ( ( ( ph -/\ th ) /\ ( ph -/\ th ) ) <-> ( ph -/\ th ) )
27		df-nan 1385	. . . . . . . . . . . . 13 |- ( ( ph -/\ th ) <-> -. ( ph /\ th ) )
28		imnan 424	. . . . . . . . . . . . . 14 |- ( ( ph -> -. th ) <-> -. ( ph /\ th ) )
29		con2b 336	. . . . . . . . . . . . . 14 |- ( ( ph -> -. th ) <-> ( th -> -. ph ) )
30	28, 29	bitr3i 255	. . . . . . . . . . . . 13 |- ( -. ( ph /\ th ) <-> ( th -> -. ph ) )
31	26, 27, 30	3bitri 275	. . . . . . . . . . . 12 |- ( ( ( ph -/\ th ) /\ ( ph -/\ th ) ) <-> ( th -> -. ph ) )
32	25, 31	xchbinx 312	. . . . . . . . . . 11 |- ( ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) <-> -. ( th -> -. ph ) )
33	24, 32	anbi12i 703	. . . . . . . . . 10 |- ( ( ( th -/\ ch ) /\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) <-> ( ( th -> -. ch ) /\ -. ( th -> -. ph ) ) )
34	33	notbii 298	. . . . . . . . 9 |- ( -. ( ( th -/\ ch ) /\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) <-> -. ( ( th -> -. ch ) /\ -. ( th -> -. ph ) ) )
35		df-nan 1385	. . . . . . . . 9 |- ( ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) <-> -. ( ( th -/\ ch ) /\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) )
36		iman 426	. . . . . . . . 9 |- ( ( ( th -> -. ch ) -> ( th -> -. ph ) ) <-> -. ( ( th -> -. ch ) /\ -. ( th -> -. ph ) ) )
37	34, 35, 36	3bitr4i 281	. . . . . . . 8 |- ( ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) <-> ( ( th -> -. ch ) -> ( th -> -. ph ) ) )
38	21, 37	anbi12i 703	. . . . . . 7 |- ( ( ( ta -/\ ( ta -/\ ta ) ) /\ ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) ) <-> ( ( ta -> ( ta /\ ta ) ) /\ ( ( th -> -. ch ) -> ( th -> -. ph ) ) ) )
39	15, 38	xchbinx 312	. . . . . 6 |- ( ( ( ta -/\ ( ta -/\ ta ) ) -/\ ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) ) <-> -. ( ( ta -> ( ta /\ ta ) ) /\ ( ( th -> -. ch ) -> ( th -> -. ph ) ) ) )
40	14, 39	anbi12i 703	. . . . 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 298	. . . 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 426	. . . 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 256	. . 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 213	. 2 |- -. ( ( ph -/\ ( ch -/\ ps ) ) /\ ( ( ta -/\ ( ta -/\ ta ) ) -/\ ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) ) )
45		df-nan 1385	. 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 213	1 |- ( ( ph -/\ ( ch -/\ ps ) ) -/\ ( ( ta -/\ ( ta -/\ ta ) ) -/\ ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 371   -/\ wnan 1384

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 189  df-an 373  df-nan 1385

This theorem is referenced by: (None)