Theorem norassOLD

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

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

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( ( 𝜑 ↔ 𝜒 ) → ( 𝜑 ↔ 𝜒 ) )
2	1	notbid	⊢ ( ( 𝜑 ↔ 𝜒 ) → ( ¬ 𝜑 ↔ ¬ 𝜒 ) )
3	2	bicomd	⊢ ( ( 𝜑 ↔ 𝜒 ) → ( ¬ 𝜒 ↔ ¬ 𝜑 ) )
4	2	anbi2d	⊢ ( ( 𝜑 ↔ 𝜒 ) → ( ( ¬ 𝜓 ∧ ¬ 𝜑 ) ↔ ( ¬ 𝜓 ∧ ¬ 𝜒 ) ) )
5	4	notbid	⊢ ( ( 𝜑 ↔ 𝜒 ) → ( ¬ ( ¬ 𝜓 ∧ ¬ 𝜑 ) ↔ ¬ ( ¬ 𝜓 ∧ ¬ 𝜒 ) ) )
6	3 5	anbi12d	⊢ ( ( 𝜑 ↔ 𝜒 ) → ( ( ¬ 𝜒 ∧ ¬ ( ¬ 𝜓 ∧ ¬ 𝜑 ) ) ↔ ( ¬ 𝜑 ∧ ¬ ( ¬ 𝜓 ∧ ¬ 𝜒 ) ) ) )
7		olc	⊢ ( 𝜑 → ( 𝜓 ∨ 𝜑 ) )
8		oran	⊢ ( ( 𝜓 ∨ 𝜑 ) ↔ ¬ ( ¬ 𝜓 ∧ ¬ 𝜑 ) )
9	7 8	sylib	⊢ ( 𝜑 → ¬ ( ¬ 𝜓 ∧ ¬ 𝜑 ) )
10	9	anim1ci	⊢ ( ( 𝜑 ∧ ¬ 𝜒 ) → ( ¬ 𝜒 ∧ ¬ ( ¬ 𝜓 ∧ ¬ 𝜑 ) ) )
11		animorl	⊢ ( ( 𝜑 ∧ ¬ 𝜒 ) → ( 𝜑 ∨ ( ¬ 𝜓 ∧ ¬ 𝜒 ) ) )
12		oran	⊢ ( ( 𝜑 ∨ ( ¬ 𝜓 ∧ ¬ 𝜒 ) ) ↔ ¬ ( ¬ 𝜑 ∧ ¬ ( ¬ 𝜓 ∧ ¬ 𝜒 ) ) )
13	11 12	sylib	⊢ ( ( 𝜑 ∧ ¬ 𝜒 ) → ¬ ( ¬ 𝜑 ∧ ¬ ( ¬ 𝜓 ∧ ¬ 𝜒 ) ) )
14	10 13	jcnd	⊢ ( ( 𝜑 ∧ ¬ 𝜒 ) → ¬ ( ( ¬ 𝜒 ∧ ¬ ( ¬ 𝜓 ∧ ¬ 𝜑 ) ) → ( ¬ 𝜑 ∧ ¬ ( ¬ 𝜓 ∧ ¬ 𝜒 ) ) ) )
15	14	ex	⊢ ( 𝜑 → ( ¬ 𝜒 → ¬ ( ( ¬ 𝜒 ∧ ¬ ( ¬ 𝜓 ∧ ¬ 𝜑 ) ) → ( ¬ 𝜑 ∧ ¬ ( ¬ 𝜓 ∧ ¬ 𝜒 ) ) ) ) )
16	15	con4d	⊢ ( 𝜑 → ( ( ( ¬ 𝜒 ∧ ¬ ( ¬ 𝜓 ∧ ¬ 𝜑 ) ) → ( ¬ 𝜑 ∧ ¬ ( ¬ 𝜓 ∧ ¬ 𝜒 ) ) ) → 𝜒 ) )
17	16	com12	⊢ ( ( ( ¬ 𝜒 ∧ ¬ ( ¬ 𝜓 ∧ ¬ 𝜑 ) ) → ( ¬ 𝜑 ∧ ¬ ( ¬ 𝜓 ∧ ¬ 𝜒 ) ) ) → ( 𝜑 → 𝜒 ) )
18		olc	⊢ ( 𝜒 → ( 𝜓 ∨ 𝜒 ) )
19		oran	⊢ ( ( 𝜓 ∨ 𝜒 ) ↔ ¬ ( ¬ 𝜓 ∧ ¬ 𝜒 ) )
20	18 19	sylib	⊢ ( 𝜒 → ¬ ( ¬ 𝜓 ∧ ¬ 𝜒 ) )
21	20	anim1ci	⊢ ( ( 𝜒 ∧ ¬ 𝜑 ) → ( ¬ 𝜑 ∧ ¬ ( ¬ 𝜓 ∧ ¬ 𝜒 ) ) )
22		animorl	⊢ ( ( 𝜒 ∧ ¬ 𝜑 ) → ( 𝜒 ∨ ( ¬ 𝜓 ∧ ¬ 𝜑 ) ) )
23		oran	⊢ ( ( 𝜒 ∨ ( ¬ 𝜓 ∧ ¬ 𝜑 ) ) ↔ ¬ ( ¬ 𝜒 ∧ ¬ ( ¬ 𝜓 ∧ ¬ 𝜑 ) ) )
24	22 23	sylib	⊢ ( ( 𝜒 ∧ ¬ 𝜑 ) → ¬ ( ¬ 𝜒 ∧ ¬ ( ¬ 𝜓 ∧ ¬ 𝜑 ) ) )
25	21 24	jcnd	⊢ ( ( 𝜒 ∧ ¬ 𝜑 ) → ¬ ( ( ¬ 𝜑 ∧ ¬ ( ¬ 𝜓 ∧ ¬ 𝜒 ) ) → ( ¬ 𝜒 ∧ ¬ ( ¬ 𝜓 ∧ ¬ 𝜑 ) ) ) )
26	25	ex	⊢ ( 𝜒 → ( ¬ 𝜑 → ¬ ( ( ¬ 𝜑 ∧ ¬ ( ¬ 𝜓 ∧ ¬ 𝜒 ) ) → ( ¬ 𝜒 ∧ ¬ ( ¬ 𝜓 ∧ ¬ 𝜑 ) ) ) ) )
27	26	con4d	⊢ ( 𝜒 → ( ( ( ¬ 𝜑 ∧ ¬ ( ¬ 𝜓 ∧ ¬ 𝜒 ) ) → ( ¬ 𝜒 ∧ ¬ ( ¬ 𝜓 ∧ ¬ 𝜑 ) ) ) → 𝜑 ) )
28	27	com12	⊢ ( ( ( ¬ 𝜑 ∧ ¬ ( ¬ 𝜓 ∧ ¬ 𝜒 ) ) → ( ¬ 𝜒 ∧ ¬ ( ¬ 𝜓 ∧ ¬ 𝜑 ) ) ) → ( 𝜒 → 𝜑 ) )
29	17 28	anim12i	⊢ ( ( ( ( ¬ 𝜒 ∧ ¬ ( ¬ 𝜓 ∧ ¬ 𝜑 ) ) → ( ¬ 𝜑 ∧ ¬ ( ¬ 𝜓 ∧ ¬ 𝜒 ) ) ) ∧ ( ( ¬ 𝜑 ∧ ¬ ( ¬ 𝜓 ∧ ¬ 𝜒 ) ) → ( ¬ 𝜒 ∧ ¬ ( ¬ 𝜓 ∧ ¬ 𝜑 ) ) ) ) → ( ( 𝜑 → 𝜒 ) ∧ ( 𝜒 → 𝜑 ) ) )
30		dfbi2	⊢ ( ( ( ¬ 𝜒 ∧ ¬ ( ¬ 𝜓 ∧ ¬ 𝜑 ) ) ↔ ( ¬ 𝜑 ∧ ¬ ( ¬ 𝜓 ∧ ¬ 𝜒 ) ) ) ↔ ( ( ( ¬ 𝜒 ∧ ¬ ( ¬ 𝜓 ∧ ¬ 𝜑 ) ) → ( ¬ 𝜑 ∧ ¬ ( ¬ 𝜓 ∧ ¬ 𝜒 ) ) ) ∧ ( ( ¬ 𝜑 ∧ ¬ ( ¬ 𝜓 ∧ ¬ 𝜒 ) ) → ( ¬ 𝜒 ∧ ¬ ( ¬ 𝜓 ∧ ¬ 𝜑 ) ) ) ) )
31		dfbi2	⊢ ( ( 𝜑 ↔ 𝜒 ) ↔ ( ( 𝜑 → 𝜒 ) ∧ ( 𝜒 → 𝜑 ) ) )
32	29 30 31	3imtr4i	⊢ ( ( ( ¬ 𝜒 ∧ ¬ ( ¬ 𝜓 ∧ ¬ 𝜑 ) ) ↔ ( ¬ 𝜑 ∧ ¬ ( ¬ 𝜓 ∧ ¬ 𝜒 ) ) ) → ( 𝜑 ↔ 𝜒 ) )
33	6 32	impbii	⊢ ( ( 𝜑 ↔ 𝜒 ) ↔ ( ( ¬ 𝜒 ∧ ¬ ( ¬ 𝜓 ∧ ¬ 𝜑 ) ) ↔ ( ¬ 𝜑 ∧ ¬ ( ¬ 𝜓 ∧ ¬ 𝜒 ) ) ) )
34		norcom	⊢ ( ( ( 𝜑 ⊽ 𝜓 ) ⊽ 𝜒 ) ↔ ( 𝜒 ⊽ ( 𝜑 ⊽ 𝜓 ) ) )
35		df-nor	⊢ ( ( 𝜒 ⊽ ( 𝜑 ⊽ 𝜓 ) ) ↔ ¬ ( 𝜒 ∨ ( 𝜑 ⊽ 𝜓 ) ) )
36		ioran	⊢ ( ¬ ( 𝜒 ∨ ( 𝜑 ⊽ 𝜓 ) ) ↔ ( ¬ 𝜒 ∧ ¬ ( 𝜑 ⊽ 𝜓 ) ) )
37		norcom	⊢ ( ( 𝜑 ⊽ 𝜓 ) ↔ ( 𝜓 ⊽ 𝜑 ) )
38		df-nor	⊢ ( ( 𝜓 ⊽ 𝜑 ) ↔ ¬ ( 𝜓 ∨ 𝜑 ) )
39		ioran	⊢ ( ¬ ( 𝜓 ∨ 𝜑 ) ↔ ( ¬ 𝜓 ∧ ¬ 𝜑 ) )
40	37 38 39	3bitri	⊢ ( ( 𝜑 ⊽ 𝜓 ) ↔ ( ¬ 𝜓 ∧ ¬ 𝜑 ) )
41	40	notbii	⊢ ( ¬ ( 𝜑 ⊽ 𝜓 ) ↔ ¬ ( ¬ 𝜓 ∧ ¬ 𝜑 ) )
42	41	anbi2i	⊢ ( ( ¬ 𝜒 ∧ ¬ ( 𝜑 ⊽ 𝜓 ) ) ↔ ( ¬ 𝜒 ∧ ¬ ( ¬ 𝜓 ∧ ¬ 𝜑 ) ) )
43	36 42	bitri	⊢ ( ¬ ( 𝜒 ∨ ( 𝜑 ⊽ 𝜓 ) ) ↔ ( ¬ 𝜒 ∧ ¬ ( ¬ 𝜓 ∧ ¬ 𝜑 ) ) )
44	34 35 43	3bitri	⊢ ( ( ( 𝜑 ⊽ 𝜓 ) ⊽ 𝜒 ) ↔ ( ¬ 𝜒 ∧ ¬ ( ¬ 𝜓 ∧ ¬ 𝜑 ) ) )
45		df-nor	⊢ ( ( 𝜑 ⊽ ( 𝜓 ⊽ 𝜒 ) ) ↔ ¬ ( 𝜑 ∨ ( 𝜓 ⊽ 𝜒 ) ) )
46		ioran	⊢ ( ¬ ( 𝜑 ∨ ( 𝜓 ⊽ 𝜒 ) ) ↔ ( ¬ 𝜑 ∧ ¬ ( 𝜓 ⊽ 𝜒 ) ) )
47		df-nor	⊢ ( ( 𝜓 ⊽ 𝜒 ) ↔ ¬ ( 𝜓 ∨ 𝜒 ) )
48		ioran	⊢ ( ¬ ( 𝜓 ∨ 𝜒 ) ↔ ( ¬ 𝜓 ∧ ¬ 𝜒 ) )
49	47 48	bitri	⊢ ( ( 𝜓 ⊽ 𝜒 ) ↔ ( ¬ 𝜓 ∧ ¬ 𝜒 ) )
50	49	notbii	⊢ ( ¬ ( 𝜓 ⊽ 𝜒 ) ↔ ¬ ( ¬ 𝜓 ∧ ¬ 𝜒 ) )
51	50	anbi2i	⊢ ( ( ¬ 𝜑 ∧ ¬ ( 𝜓 ⊽ 𝜒 ) ) ↔ ( ¬ 𝜑 ∧ ¬ ( ¬ 𝜓 ∧ ¬ 𝜒 ) ) )
52	45 46 51	3bitri	⊢ ( ( 𝜑 ⊽ ( 𝜓 ⊽ 𝜒 ) ) ↔ ( ¬ 𝜑 ∧ ¬ ( ¬ 𝜓 ∧ ¬ 𝜒 ) ) )
53	44 52	bibi12i	⊢ ( ( ( ( 𝜑 ⊽ 𝜓 ) ⊽ 𝜒 ) ↔ ( 𝜑 ⊽ ( 𝜓 ⊽ 𝜒 ) ) ) ↔ ( ( ¬ 𝜒 ∧ ¬ ( ¬ 𝜓 ∧ ¬ 𝜑 ) ) ↔ ( ¬ 𝜑 ∧ ¬ ( ¬ 𝜓 ∧ ¬ 𝜒 ) ) ) )
54	33 53	bitr4i	⊢ ( ( 𝜑 ↔ 𝜒 ) ↔ ( ( ( 𝜑 ⊽ 𝜓 ) ⊽ 𝜒 ) ↔ ( 𝜑 ⊽ ( 𝜓 ⊽ 𝜒 ) ) ) )