Theorem norassOLD 1536

Description: Obsolete version of norass 1535 as of 17-Dec-2023. (Contributed by RP, 29-Oct-2023.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
norassOLD	⊢ ((𝜑 ↔ 𝜒) ↔ (((𝜑 ⊽ 𝜓) ⊽ 𝜒) ↔ (𝜑 ⊽ (𝜓 ⊽ 𝜒))))

Proof of Theorem norassOLD

Step	Hyp	Ref	Expression
1		id 22	. . . . . 6 ⊢ ((𝜑 ↔ 𝜒) → (𝜑 ↔ 𝜒))
2	1	notbid 318	. . . . 5 ⊢ ((𝜑 ↔ 𝜒) → (¬ 𝜑 ↔ ¬ 𝜒))
3	2	bicomd 222	. . . 4 ⊢ ((𝜑 ↔ 𝜒) → (¬ 𝜒 ↔ ¬ 𝜑))
4	2	anbi2d 629	. . . . 5 ⊢ ((𝜑 ↔ 𝜒) → ((¬ 𝜓 ∧ ¬ 𝜑) ↔ (¬ 𝜓 ∧ ¬ 𝜒)))
5	4	notbid 318	. . . 4 ⊢ ((𝜑 ↔ 𝜒) → (¬ (¬ 𝜓 ∧ ¬ 𝜑) ↔ ¬ (¬ 𝜓 ∧ ¬ 𝜒)))
6	3, 5	anbi12d 631	. . 3 ⊢ ((𝜑 ↔ 𝜒) → ((¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)) ↔ (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒))))
7		olc 865	. . . . . . . . . . 11 ⊢ (𝜑 → (𝜓 ∨ 𝜑))
8		oran 987	. . . . . . . . . . 11 ⊢ ((𝜓 ∨ 𝜑) ↔ ¬ (¬ 𝜓 ∧ ¬ 𝜑))
9	7, 8	sylib 217	. . . . . . . . . 10 ⊢ (𝜑 → ¬ (¬ 𝜓 ∧ ¬ 𝜑))
10	9	anim1ci 616	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝜒) → (¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)))
11		animorl 975	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝜒) → (𝜑 ∨ (¬ 𝜓 ∧ ¬ 𝜒)))
12		oran 987	. . . . . . . . . 10 ⊢ ((𝜑 ∨ (¬ 𝜓 ∧ ¬ 𝜒)) ↔ ¬ (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒)))
13	11, 12	sylib 217	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝜒) → ¬ (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒)))
14	10, 13	jcnd 163	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝜒) → ¬ ((¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)) → (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒))))
15	14	ex 413	. . . . . . 7 ⊢ (𝜑 → (¬ 𝜒 → ¬ ((¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)) → (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒)))))
16	15	con4d 115	. . . . . 6 ⊢ (𝜑 → (((¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)) → (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒))) → 𝜒))
17	16	com12 32	. . . . 5 ⊢ (((¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)) → (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒))) → (𝜑 → 𝜒))
18		olc 865	. . . . . . . . . . 11 ⊢ (𝜒 → (𝜓 ∨ 𝜒))
19		oran 987	. . . . . . . . . . 11 ⊢ ((𝜓 ∨ 𝜒) ↔ ¬ (¬ 𝜓 ∧ ¬ 𝜒))
20	18, 19	sylib 217	. . . . . . . . . 10 ⊢ (𝜒 → ¬ (¬ 𝜓 ∧ ¬ 𝜒))
21	20	anim1ci 616	. . . . . . . . 9 ⊢ ((𝜒 ∧ ¬ 𝜑) → (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒)))
22		animorl 975	. . . . . . . . . 10 ⊢ ((𝜒 ∧ ¬ 𝜑) → (𝜒 ∨ (¬ 𝜓 ∧ ¬ 𝜑)))
23		oran 987	. . . . . . . . . 10 ⊢ ((𝜒 ∨ (¬ 𝜓 ∧ ¬ 𝜑)) ↔ ¬ (¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)))
24	22, 23	sylib 217	. . . . . . . . 9 ⊢ ((𝜒 ∧ ¬ 𝜑) → ¬ (¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)))
25	21, 24	jcnd 163	. . . . . . . 8 ⊢ ((𝜒 ∧ ¬ 𝜑) → ¬ ((¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒)) → (¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑))))
26	25	ex 413	. . . . . . 7 ⊢ (𝜒 → (¬ 𝜑 → ¬ ((¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒)) → (¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)))))
27	26	con4d 115	. . . . . 6 ⊢ (𝜒 → (((¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒)) → (¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑))) → 𝜑))
28	27	com12 32	. . . . 5 ⊢ (((¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒)) → (¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑))) → (𝜒 → 𝜑))
29	17, 28	anim12i 613	. . . 4 ⊢ ((((¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)) → (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒))) ∧ ((¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒)) → (¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)))) → ((𝜑 → 𝜒) ∧ (𝜒 → 𝜑)))
30		dfbi2 475	. . . 4 ⊢ (((¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)) ↔ (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒))) ↔ (((¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)) → (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒))) ∧ ((¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒)) → (¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)))))
31		dfbi2 475	. . . 4 ⊢ ((𝜑 ↔ 𝜒) ↔ ((𝜑 → 𝜒) ∧ (𝜒 → 𝜑)))
32	29, 30, 31	3imtr4i 292	. . 3 ⊢ (((¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)) ↔ (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒))) → (𝜑 ↔ 𝜒))
33	6, 32	impbii 208	. 2 ⊢ ((𝜑 ↔ 𝜒) ↔ ((¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)) ↔ (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒))))
34		norcom 1527	. . . 4 ⊢ (((𝜑 ⊽ 𝜓) ⊽ 𝜒) ↔ (𝜒 ⊽ (𝜑 ⊽ 𝜓)))
35		df-nor 1526	. . . 4 ⊢ ((𝜒 ⊽ (𝜑 ⊽ 𝜓)) ↔ ¬ (𝜒 ∨ (𝜑 ⊽ 𝜓)))
36		ioran 981	. . . . 5 ⊢ (¬ (𝜒 ∨ (𝜑 ⊽ 𝜓)) ↔ (¬ 𝜒 ∧ ¬ (𝜑 ⊽ 𝜓)))
37		norcom 1527	. . . . . . . 8 ⊢ ((𝜑 ⊽ 𝜓) ↔ (𝜓 ⊽ 𝜑))
38		df-nor 1526	. . . . . . . 8 ⊢ ((𝜓 ⊽ 𝜑) ↔ ¬ (𝜓 ∨ 𝜑))
39		ioran 981	. . . . . . . 8 ⊢ (¬ (𝜓 ∨ 𝜑) ↔ (¬ 𝜓 ∧ ¬ 𝜑))
40	37, 38, 39	3bitri 297	. . . . . . 7 ⊢ ((𝜑 ⊽ 𝜓) ↔ (¬ 𝜓 ∧ ¬ 𝜑))
41	40	notbii 320	. . . . . 6 ⊢ (¬ (𝜑 ⊽ 𝜓) ↔ ¬ (¬ 𝜓 ∧ ¬ 𝜑))
42	41	anbi2i 623	. . . . 5 ⊢ ((¬ 𝜒 ∧ ¬ (𝜑 ⊽ 𝜓)) ↔ (¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)))
43	36, 42	bitri 274	. . . 4 ⊢ (¬ (𝜒 ∨ (𝜑 ⊽ 𝜓)) ↔ (¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)))
44	34, 35, 43	3bitri 297	. . 3 ⊢ (((𝜑 ⊽ 𝜓) ⊽ 𝜒) ↔ (¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)))
45		df-nor 1526	. . . 4 ⊢ ((𝜑 ⊽ (𝜓 ⊽ 𝜒)) ↔ ¬ (𝜑 ∨ (𝜓 ⊽ 𝜒)))
46		ioran 981	. . . 4 ⊢ (¬ (𝜑 ∨ (𝜓 ⊽ 𝜒)) ↔ (¬ 𝜑 ∧ ¬ (𝜓 ⊽ 𝜒)))
47		df-nor 1526	. . . . . . 7 ⊢ ((𝜓 ⊽ 𝜒) ↔ ¬ (𝜓 ∨ 𝜒))
48		ioran 981	. . . . . . 7 ⊢ (¬ (𝜓 ∨ 𝜒) ↔ (¬ 𝜓 ∧ ¬ 𝜒))
49	47, 48	bitri 274	. . . . . 6 ⊢ ((𝜓 ⊽ 𝜒) ↔ (¬ 𝜓 ∧ ¬ 𝜒))
50	49	notbii 320	. . . . 5 ⊢ (¬ (𝜓 ⊽ 𝜒) ↔ ¬ (¬ 𝜓 ∧ ¬ 𝜒))
51	50	anbi2i 623	. . . 4 ⊢ ((¬ 𝜑 ∧ ¬ (𝜓 ⊽ 𝜒)) ↔ (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒)))
52	45, 46, 51	3bitri 297	. . 3 ⊢ ((𝜑 ⊽ (𝜓 ⊽ 𝜒)) ↔ (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒)))
53	44, 52	bibi12i 340	. 2 ⊢ ((((𝜑 ⊽ 𝜓) ⊽ 𝜒) ↔ (𝜑 ⊽ (𝜓 ⊽ 𝜒))) ↔ ((¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)) ↔ (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒))))
54	33, 53	bitr4i 277	1 ⊢ ((𝜑 ↔ 𝜒) ↔ (((𝜑 ⊽ 𝜓) ⊽ 𝜒) ↔ (𝜑 ⊽ (𝜓 ⊽ 𝜒))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 844   ⊽ wnor 1525

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 206  df-an 397  df-or 845  df-nor 1526

This theorem is referenced by: (None)