Theorem nic-axALT 1707

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

Assertion

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

Proof of Theorem nic-axALT

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ⊼ wnan 1521

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-nan 1522

This theorem is used by: (None)