Theorem norassOLD 1534

Description: Obsolete version of norass 1533 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 320	. . . . 5 ⊢ ((𝜑 ↔ 𝜒) → (¬ 𝜑 ↔ ¬ 𝜒))
3	2	bicomd 225	. . . 4 ⊢ ((𝜑 ↔ 𝜒) → (¬ 𝜒 ↔ ¬ 𝜑))
4	2	anbi2d 630	. . . . 5 ⊢ ((𝜑 ↔ 𝜒) → ((¬ 𝜓 ∧ ¬ 𝜑) ↔ (¬ 𝜓 ∧ ¬ 𝜒)))
5	4	notbid 320	. . . 4 ⊢ ((𝜑 ↔ 𝜒) → (¬ (¬ 𝜓 ∧ ¬ 𝜑) ↔ ¬ (¬ 𝜓 ∧ ¬ 𝜒)))
6	3, 5	anbi12d 632	. . 3 ⊢ ((𝜑 ↔ 𝜒) → ((¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)) ↔ (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒))))
7		olc 864	. . . . . . . . . . 11 ⊢ (𝜑 → (𝜓 ∨ 𝜑))
8		oran 986	. . . . . . . . . . 11 ⊢ ((𝜓 ∨ 𝜑) ↔ ¬ (¬ 𝜓 ∧ ¬ 𝜑))
9	7, 8	sylib 220	. . . . . . . . . 10 ⊢ (𝜑 → ¬ (¬ 𝜓 ∧ ¬ 𝜑))
10	9	anim1ci 617	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝜒) → (¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)))
11		animorl 974	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝜒) → (𝜑 ∨ (¬ 𝜓 ∧ ¬ 𝜒)))
12		oran 986	. . . . . . . . . 10 ⊢ ((𝜑 ∨ (¬ 𝜓 ∧ ¬ 𝜒)) ↔ ¬ (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒)))
13	11, 12	sylib 220	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝜒) → ¬ (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒)))
14	10, 13	jcnd 165	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝜒) → ¬ ((¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)) → (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒))))
15	14	ex 415	. . . . . . 7 ⊢ (𝜑 → (¬ 𝜒 → ¬ ((¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)) → (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒)))))
16	15	con4d 115	. . . . . 6 ⊢ (𝜑 → (((¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)) → (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒))) → 𝜒))
17	16	com12 32	. . . . 5 ⊢ (((¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)) → (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒))) → (𝜑 → 𝜒))
18		olc 864	. . . . . . . . . . 11 ⊢ (𝜒 → (𝜓 ∨ 𝜒))
19		oran 986	. . . . . . . . . . 11 ⊢ ((𝜓 ∨ 𝜒) ↔ ¬ (¬ 𝜓 ∧ ¬ 𝜒))
20	18, 19	sylib 220	. . . . . . . . . 10 ⊢ (𝜒 → ¬ (¬ 𝜓 ∧ ¬ 𝜒))
21	20	anim1ci 617	. . . . . . . . 9 ⊢ ((𝜒 ∧ ¬ 𝜑) → (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒)))
22		animorl 974	. . . . . . . . . 10 ⊢ ((𝜒 ∧ ¬ 𝜑) → (𝜒 ∨ (¬ 𝜓 ∧ ¬ 𝜑)))
23		oran 986	. . . . . . . . . 10 ⊢ ((𝜒 ∨ (¬ 𝜓 ∧ ¬ 𝜑)) ↔ ¬ (¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)))
24	22, 23	sylib 220	. . . . . . . . 9 ⊢ ((𝜒 ∧ ¬ 𝜑) → ¬ (¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)))
25	21, 24	jcnd 165	. . . . . . . 8 ⊢ ((𝜒 ∧ ¬ 𝜑) → ¬ ((¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒)) → (¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑))))
26	25	ex 415	. . . . . . 7 ⊢ (𝜒 → (¬ 𝜑 → ¬ ((¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒)) → (¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)))))
27	26	con4d 115	. . . . . 6 ⊢ (𝜒 → (((¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒)) → (¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑))) → 𝜑))
28	27	com12 32	. . . . 5 ⊢ (((¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒)) → (¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑))) → (𝜒 → 𝜑))
29	17, 28	anim12i 614	. . . 4 ⊢ ((((¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)) → (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒))) ∧ ((¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒)) → (¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)))) → ((𝜑 → 𝜒) ∧ (𝜒 → 𝜑)))
30		dfbi2 477	. . . 4 ⊢ (((¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)) ↔ (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒))) ↔ (((¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)) → (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒))) ∧ ((¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒)) → (¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)))))
31		dfbi2 477	. . . 4 ⊢ ((𝜑 ↔ 𝜒) ↔ ((𝜑 → 𝜒) ∧ (𝜒 → 𝜑)))
32	29, 30, 31	3imtr4i 294	. . 3 ⊢ (((¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)) ↔ (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒))) → (𝜑 ↔ 𝜒))
33	6, 32	impbii 211	. 2 ⊢ ((𝜑 ↔ 𝜒) ↔ ((¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)) ↔ (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒))))
34		norcom 1522	. . . 4 ⊢ (((𝜑 ⊽ 𝜓) ⊽ 𝜒) ↔ (𝜒 ⊽ (𝜑 ⊽ 𝜓)))
35		df-nor 1521	. . . 4 ⊢ ((𝜒 ⊽ (𝜑 ⊽ 𝜓)) ↔ ¬ (𝜒 ∨ (𝜑 ⊽ 𝜓)))
36		ioran 980	. . . . 5 ⊢ (¬ (𝜒 ∨ (𝜑 ⊽ 𝜓)) ↔ (¬ 𝜒 ∧ ¬ (𝜑 ⊽ 𝜓)))
37		norcom 1522	. . . . . . . 8 ⊢ ((𝜑 ⊽ 𝜓) ↔ (𝜓 ⊽ 𝜑))
38		df-nor 1521	. . . . . . . 8 ⊢ ((𝜓 ⊽ 𝜑) ↔ ¬ (𝜓 ∨ 𝜑))
39		ioran 980	. . . . . . . 8 ⊢ (¬ (𝜓 ∨ 𝜑) ↔ (¬ 𝜓 ∧ ¬ 𝜑))
40	37, 38, 39	3bitri 299	. . . . . . 7 ⊢ ((𝜑 ⊽ 𝜓) ↔ (¬ 𝜓 ∧ ¬ 𝜑))
41	40	notbii 322	. . . . . 6 ⊢ (¬ (𝜑 ⊽ 𝜓) ↔ ¬ (¬ 𝜓 ∧ ¬ 𝜑))
42	41	anbi2i 624	. . . . 5 ⊢ ((¬ 𝜒 ∧ ¬ (𝜑 ⊽ 𝜓)) ↔ (¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)))
43	36, 42	bitri 277	. . . 4 ⊢ (¬ (𝜒 ∨ (𝜑 ⊽ 𝜓)) ↔ (¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)))
44	34, 35, 43	3bitri 299	. . 3 ⊢ (((𝜑 ⊽ 𝜓) ⊽ 𝜒) ↔ (¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)))
45		df-nor 1521	. . . 4 ⊢ ((𝜑 ⊽ (𝜓 ⊽ 𝜒)) ↔ ¬ (𝜑 ∨ (𝜓 ⊽ 𝜒)))
46		ioran 980	. . . 4 ⊢ (¬ (𝜑 ∨ (𝜓 ⊽ 𝜒)) ↔ (¬ 𝜑 ∧ ¬ (𝜓 ⊽ 𝜒)))
47		df-nor 1521	. . . . . . 7 ⊢ ((𝜓 ⊽ 𝜒) ↔ ¬ (𝜓 ∨ 𝜒))
48		ioran 980	. . . . . . 7 ⊢ (¬ (𝜓 ∨ 𝜒) ↔ (¬ 𝜓 ∧ ¬ 𝜒))
49	47, 48	bitri 277	. . . . . 6 ⊢ ((𝜓 ⊽ 𝜒) ↔ (¬ 𝜓 ∧ ¬ 𝜒))
50	49	notbii 322	. . . . 5 ⊢ (¬ (𝜓 ⊽ 𝜒) ↔ ¬ (¬ 𝜓 ∧ ¬ 𝜒))
51	50	anbi2i 624	. . . 4 ⊢ ((¬ 𝜑 ∧ ¬ (𝜓 ⊽ 𝜒)) ↔ (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒)))
52	45, 46, 51	3bitri 299	. . 3 ⊢ ((𝜑 ⊽ (𝜓 ⊽ 𝜒)) ↔ (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒)))
53	44, 52	bibi12i 342	. 2 ⊢ ((((𝜑 ⊽ 𝜓) ⊽ 𝜒) ↔ (𝜑 ⊽ (𝜓 ⊽ 𝜒))) ↔ ((¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)) ↔ (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒))))
54	33, 53	bitr4i 280	1 ⊢ ((𝜑 ↔ 𝜒) ↔ (((𝜑 ⊽ 𝜓) ⊽ 𝜒) ↔ (𝜑 ⊽ (𝜓 ⊽ 𝜒))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∨ wo 843   ⊽ wnor 1520

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 209  df-an 399  df-or 844  df-nor 1521

This theorem is referenced by: (None)