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	$⊢ (φ \leftrightarrow χ) \leftrightarrow (((φ ⊽ ψ) ⊽ χ) \leftrightarrow (φ ⊽ (ψ ⊽ χ)))$

Proof

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

Metamath Proof Explorer

Theorem norassOLD

Proof