Theorem nic-axALT

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

	Ref	Expression
Assertion	nic-axALT	⊢ ( ( 𝜑 ⊼ ( 𝜒 ⊼ 𝜓 ) ) ⊼ ( ( 𝜏 ⊼ ( 𝜏 ⊼ 𝜏 ) ) ⊼ ( ( 𝜃 ⊼ 𝜒 ) ⊼ ( ( 𝜑 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝜒 ∧ 𝜓 ) → 𝜒 )
2	1	imim2i	⊢ ( ( 𝜑 → ( 𝜒 ∧ 𝜓 ) ) → ( 𝜑 → 𝜒 ) )
3		con3	⊢ ( ( 𝜑 → 𝜒 ) → ( ¬ 𝜒 → ¬ 𝜑 ) )
4	3	imim2d	⊢ ( ( 𝜑 → 𝜒 ) → ( ( 𝜃 → ¬ 𝜒 ) → ( 𝜃 → ¬ 𝜑 ) ) )
5	2 4	syl	⊢ ( ( 𝜑 → ( 𝜒 ∧ 𝜓 ) ) → ( ( 𝜃 → ¬ 𝜒 ) → ( 𝜃 → ¬ 𝜑 ) ) )
6		anidm	⊢ ( ( 𝜏 ∧ 𝜏 ) ↔ 𝜏 )
7	6	biimpri	⊢ ( 𝜏 → ( 𝜏 ∧ 𝜏 ) )
8	5 7	jctil	⊢ ( ( 𝜑 → ( 𝜒 ∧ 𝜓 ) ) → ( ( 𝜏 → ( 𝜏 ∧ 𝜏 ) ) ∧ ( ( 𝜃 → ¬ 𝜒 ) → ( 𝜃 → ¬ 𝜑 ) ) ) )
9		df-nan	⊢ ( ( 𝜒 ⊼ 𝜓 ) ↔ ¬ ( 𝜒 ∧ 𝜓 ) )
10	9	anbi2i	⊢ ( ( 𝜑 ∧ ( 𝜒 ⊼ 𝜓 ) ) ↔ ( 𝜑 ∧ ¬ ( 𝜒 ∧ 𝜓 ) ) )
11	10	notbii	⊢ ( ¬ ( 𝜑 ∧ ( 𝜒 ⊼ 𝜓 ) ) ↔ ¬ ( 𝜑 ∧ ¬ ( 𝜒 ∧ 𝜓 ) ) )
12		df-nan	⊢ ( ( 𝜑 ⊼ ( 𝜒 ⊼ 𝜓 ) ) ↔ ¬ ( 𝜑 ∧ ( 𝜒 ⊼ 𝜓 ) ) )
13		iman	⊢ ( ( 𝜑 → ( 𝜒 ∧ 𝜓 ) ) ↔ ¬ ( 𝜑 ∧ ¬ ( 𝜒 ∧ 𝜓 ) ) )
14	11 12 13	3bitr4i	⊢ ( ( 𝜑 ⊼ ( 𝜒 ⊼ 𝜓 ) ) ↔ ( 𝜑 → ( 𝜒 ∧ 𝜓 ) ) )
15		df-nan	⊢ ( ( ( 𝜏 ⊼ ( 𝜏 ⊼ 𝜏 ) ) ⊼ ( ( 𝜃 ⊼ 𝜒 ) ⊼ ( ( 𝜑 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ) ) ↔ ¬ ( ( 𝜏 ⊼ ( 𝜏 ⊼ 𝜏 ) ) ∧ ( ( 𝜃 ⊼ 𝜒 ) ⊼ ( ( 𝜑 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ) ) )
16		df-nan	⊢ ( ( 𝜏 ⊼ 𝜏 ) ↔ ¬ ( 𝜏 ∧ 𝜏 ) )
17	16	anbi2i	⊢ ( ( 𝜏 ∧ ( 𝜏 ⊼ 𝜏 ) ) ↔ ( 𝜏 ∧ ¬ ( 𝜏 ∧ 𝜏 ) ) )
18	17	notbii	⊢ ( ¬ ( 𝜏 ∧ ( 𝜏 ⊼ 𝜏 ) ) ↔ ¬ ( 𝜏 ∧ ¬ ( 𝜏 ∧ 𝜏 ) ) )
19		df-nan	⊢ ( ( 𝜏 ⊼ ( 𝜏 ⊼ 𝜏 ) ) ↔ ¬ ( 𝜏 ∧ ( 𝜏 ⊼ 𝜏 ) ) )
20		iman	⊢ ( ( 𝜏 → ( 𝜏 ∧ 𝜏 ) ) ↔ ¬ ( 𝜏 ∧ ¬ ( 𝜏 ∧ 𝜏 ) ) )
21	18 19 20	3bitr4i	⊢ ( ( 𝜏 ⊼ ( 𝜏 ⊼ 𝜏 ) ) ↔ ( 𝜏 → ( 𝜏 ∧ 𝜏 ) ) )
22		df-nan	⊢ ( ( 𝜃 ⊼ 𝜒 ) ↔ ¬ ( 𝜃 ∧ 𝜒 ) )
23		imnan	⊢ ( ( 𝜃 → ¬ 𝜒 ) ↔ ¬ ( 𝜃 ∧ 𝜒 ) )
24	22 23	bitr4i	⊢ ( ( 𝜃 ⊼ 𝜒 ) ↔ ( 𝜃 → ¬ 𝜒 ) )
25		df-nan	⊢ ( ( ( 𝜑 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ↔ ¬ ( ( 𝜑 ⊼ 𝜃 ) ∧ ( 𝜑 ⊼ 𝜃 ) ) )
26		anidm	⊢ ( ( ( 𝜑 ⊼ 𝜃 ) ∧ ( 𝜑 ⊼ 𝜃 ) ) ↔ ( 𝜑 ⊼ 𝜃 ) )
27		df-nan	⊢ ( ( 𝜑 ⊼ 𝜃 ) ↔ ¬ ( 𝜑 ∧ 𝜃 ) )
28		imnan	⊢ ( ( 𝜑 → ¬ 𝜃 ) ↔ ¬ ( 𝜑 ∧ 𝜃 ) )
29		con2b	⊢ ( ( 𝜑 → ¬ 𝜃 ) ↔ ( 𝜃 → ¬ 𝜑 ) )
30	28 29	bitr3i	⊢ ( ¬ ( 𝜑 ∧ 𝜃 ) ↔ ( 𝜃 → ¬ 𝜑 ) )
31	26 27 30	3bitri	⊢ ( ( ( 𝜑 ⊼ 𝜃 ) ∧ ( 𝜑 ⊼ 𝜃 ) ) ↔ ( 𝜃 → ¬ 𝜑 ) )
32	25 31	xchbinx	⊢ ( ( ( 𝜑 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ↔ ¬ ( 𝜃 → ¬ 𝜑 ) )
33	24 32	anbi12i	⊢ ( ( ( 𝜃 ⊼ 𝜒 ) ∧ ( ( 𝜑 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ) ↔ ( ( 𝜃 → ¬ 𝜒 ) ∧ ¬ ( 𝜃 → ¬ 𝜑 ) ) )
34	33	notbii	⊢ ( ¬ ( ( 𝜃 ⊼ 𝜒 ) ∧ ( ( 𝜑 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ) ↔ ¬ ( ( 𝜃 → ¬ 𝜒 ) ∧ ¬ ( 𝜃 → ¬ 𝜑 ) ) )
35		df-nan	⊢ ( ( ( 𝜃 ⊼ 𝜒 ) ⊼ ( ( 𝜑 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ) ↔ ¬ ( ( 𝜃 ⊼ 𝜒 ) ∧ ( ( 𝜑 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ) )
36		iman	⊢ ( ( ( 𝜃 → ¬ 𝜒 ) → ( 𝜃 → ¬ 𝜑 ) ) ↔ ¬ ( ( 𝜃 → ¬ 𝜒 ) ∧ ¬ ( 𝜃 → ¬ 𝜑 ) ) )
37	34 35 36	3bitr4i	⊢ ( ( ( 𝜃 ⊼ 𝜒 ) ⊼ ( ( 𝜑 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ) ↔ ( ( 𝜃 → ¬ 𝜒 ) → ( 𝜃 → ¬ 𝜑 ) ) )
38	21 37	anbi12i	⊢ ( ( ( 𝜏 ⊼ ( 𝜏 ⊼ 𝜏 ) ) ∧ ( ( 𝜃 ⊼ 𝜒 ) ⊼ ( ( 𝜑 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ) ) ↔ ( ( 𝜏 → ( 𝜏 ∧ 𝜏 ) ) ∧ ( ( 𝜃 → ¬ 𝜒 ) → ( 𝜃 → ¬ 𝜑 ) ) ) )
39	15 38	xchbinx	⊢ ( ( ( 𝜏 ⊼ ( 𝜏 ⊼ 𝜏 ) ) ⊼ ( ( 𝜃 ⊼ 𝜒 ) ⊼ ( ( 𝜑 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ) ) ↔ ¬ ( ( 𝜏 → ( 𝜏 ∧ 𝜏 ) ) ∧ ( ( 𝜃 → ¬ 𝜒 ) → ( 𝜃 → ¬ 𝜑 ) ) ) )
40	14 39	anbi12i	⊢ ( ( ( 𝜑 ⊼ ( 𝜒 ⊼ 𝜓 ) ) ∧ ( ( 𝜏 ⊼ ( 𝜏 ⊼ 𝜏 ) ) ⊼ ( ( 𝜃 ⊼ 𝜒 ) ⊼ ( ( 𝜑 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ) ) ) ↔ ( ( 𝜑 → ( 𝜒 ∧ 𝜓 ) ) ∧ ¬ ( ( 𝜏 → ( 𝜏 ∧ 𝜏 ) ) ∧ ( ( 𝜃 → ¬ 𝜒 ) → ( 𝜃 → ¬ 𝜑 ) ) ) ) )
41	40	notbii	⊢ ( ¬ ( ( 𝜑 ⊼ ( 𝜒 ⊼ 𝜓 ) ) ∧ ( ( 𝜏 ⊼ ( 𝜏 ⊼ 𝜏 ) ) ⊼ ( ( 𝜃 ⊼ 𝜒 ) ⊼ ( ( 𝜑 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ) ) ) ↔ ¬ ( ( 𝜑 → ( 𝜒 ∧ 𝜓 ) ) ∧ ¬ ( ( 𝜏 → ( 𝜏 ∧ 𝜏 ) ) ∧ ( ( 𝜃 → ¬ 𝜒 ) → ( 𝜃 → ¬ 𝜑 ) ) ) ) )
42		iman	⊢ ( ( ( 𝜑 → ( 𝜒 ∧ 𝜓 ) ) → ( ( 𝜏 → ( 𝜏 ∧ 𝜏 ) ) ∧ ( ( 𝜃 → ¬ 𝜒 ) → ( 𝜃 → ¬ 𝜑 ) ) ) ) ↔ ¬ ( ( 𝜑 → ( 𝜒 ∧ 𝜓 ) ) ∧ ¬ ( ( 𝜏 → ( 𝜏 ∧ 𝜏 ) ) ∧ ( ( 𝜃 → ¬ 𝜒 ) → ( 𝜃 → ¬ 𝜑 ) ) ) ) )
43	41 42	bitr4i	⊢ ( ¬ ( ( 𝜑 ⊼ ( 𝜒 ⊼ 𝜓 ) ) ∧ ( ( 𝜏 ⊼ ( 𝜏 ⊼ 𝜏 ) ) ⊼ ( ( 𝜃 ⊼ 𝜒 ) ⊼ ( ( 𝜑 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ) ) ) ↔ ( ( 𝜑 → ( 𝜒 ∧ 𝜓 ) ) → ( ( 𝜏 → ( 𝜏 ∧ 𝜏 ) ) ∧ ( ( 𝜃 → ¬ 𝜒 ) → ( 𝜃 → ¬ 𝜑 ) ) ) ) )
44	8 43	mpbir	⊢ ¬ ( ( 𝜑 ⊼ ( 𝜒 ⊼ 𝜓 ) ) ∧ ( ( 𝜏 ⊼ ( 𝜏 ⊼ 𝜏 ) ) ⊼ ( ( 𝜃 ⊼ 𝜒 ) ⊼ ( ( 𝜑 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ) ) )
45		df-nan	⊢ ( ( ( 𝜑 ⊼ ( 𝜒 ⊼ 𝜓 ) ) ⊼ ( ( 𝜏 ⊼ ( 𝜏 ⊼ 𝜏 ) ) ⊼ ( ( 𝜃 ⊼ 𝜒 ) ⊼ ( ( 𝜑 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ) ) ) ↔ ¬ ( ( 𝜑 ⊼ ( 𝜒 ⊼ 𝜓 ) ) ∧ ( ( 𝜏 ⊼ ( 𝜏 ⊼ 𝜏 ) ) ⊼ ( ( 𝜃 ⊼ 𝜒 ) ⊼ ( ( 𝜑 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ) ) ) )
46	44 45	mpbir	⊢ ( ( 𝜑 ⊼ ( 𝜒 ⊼ 𝜓 ) ) ⊼ ( ( 𝜏 ⊼ ( 𝜏 ⊼ 𝜏 ) ) ⊼ ( ( 𝜃 ⊼ 𝜒 ) ⊼ ( ( 𝜑 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ) ) )