Theorem u3lem13b 790

Description: Lemma for unified implication study. (Contributed by NM, 19-Jan-1998.)

Assertion

Ref	Expression
u3lem13b	((a →3 b⊥ ) →3 a⊥ ) = (a →1 b)

Proof of Theorem u3lem13b

Step	Hyp	Ref	Expression
1		df-i3 46	. 2 ((a →3 b⊥ ) →3 a⊥ ) = ((((a →3 b⊥ )⊥ ∩ a⊥ ) ∪ ((a →3 b⊥ )⊥ ∩ a⊥ ⊥ )) ∪ ((a →3 b⊥ ) ∩ ((a →3 b⊥ )⊥ ∪ a⊥ )))
2		u3lemnana 647	. . . . . 6 ((a →3 b⊥ )⊥ ∩ a⊥ ) = (a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )))
3		ax-a1 30	. . . . . . . . 9 a = a⊥ ⊥
4	3	ax-r1 35	. . . . . . . 8 a⊥ ⊥ = a
5	4	lan 77	. . . . . . 7 ((a →3 b⊥ )⊥ ∩ a⊥ ⊥ ) = ((a →3 b⊥ )⊥ ∩ a)
6		u3lemnaa 642	. . . . . . 7 ((a →3 b⊥ )⊥ ∩ a) = (a ∩ b⊥ ⊥ )
7	5, 6	ax-r2 36	. . . . . 6 ((a →3 b⊥ )⊥ ∩ a⊥ ⊥ ) = (a ∩ b⊥ ⊥ )
8	2, 7	2or 72	. . . . 5 (((a →3 b⊥ )⊥ ∩ a⊥ ) ∪ ((a →3 b⊥ )⊥ ∩ a⊥ ⊥ )) = ((a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))) ∪ (a ∩ b⊥ ⊥ ))
9		comanr1 464	. . . . . . . 8 a C (a ∩ b⊥ ⊥ )
10	9	comcom3 454	. . . . . . 7 a⊥ C (a ∩ b⊥ ⊥ )
11		comorr 184	. . . . . . . . 9 a C (a ∪ b⊥ )
12		comorr 184	. . . . . . . . 9 a C (a ∪ b⊥ ⊥ )
13	11, 12	com2an 484	. . . . . . . 8 a C ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))
14	13	comcom3 454	. . . . . . 7 a⊥ C ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))
15	10, 14	fh4r 476	. . . . . 6 ((a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))) ∪ (a ∩ b⊥ ⊥ )) = ((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∩ (((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) ∪ (a ∩ b⊥ ⊥ )))
16		coman1 185	. . . . . . . . . 10 (a ∩ b⊥ ⊥ ) C a
17		coman2 186	. . . . . . . . . . 11 (a ∩ b⊥ ⊥ ) C b⊥ ⊥
18	17	comcom7 460	. . . . . . . . . 10 (a ∩ b⊥ ⊥ ) C b⊥
19	16, 18	com2or 483	. . . . . . . . 9 (a ∩ b⊥ ⊥ ) C (a ∪ b⊥ )
20	16, 17	com2or 483	. . . . . . . . 9 (a ∩ b⊥ ⊥ ) C (a ∪ b⊥ ⊥ )
21	19, 20	fh3r 475	. . . . . . . 8 (((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) ∪ (a ∩ b⊥ ⊥ )) = (((a ∪ b⊥ ) ∪ (a ∩ b⊥ ⊥ )) ∩ ((a ∪ b⊥ ⊥ ) ∪ (a ∩ b⊥ ⊥ )))
22	21	lan 77	. . . . . . 7 ((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∩ (((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) ∪ (a ∩ b⊥ ⊥ ))) = ((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∩ (((a ∪ b⊥ ) ∪ (a ∩ b⊥ ⊥ )) ∩ ((a ∪ b⊥ ⊥ ) ∪ (a ∩ b⊥ ⊥ ))))
23		ax-a2 31	. . . . . . . . . . . 12 ((a ∪ b⊥ ) ∪ (a ∩ b⊥ ⊥ )) = ((a ∩ b⊥ ⊥ ) ∪ (a ∪ b⊥ ))
24		lea 160	. . . . . . . . . . . . . 14 (a ∩ b⊥ ⊥ ) ≤ a
25		leo 158	. . . . . . . . . . . . . 14 a ≤ (a ∪ b⊥ )
26	24, 25	letr 137	. . . . . . . . . . . . 13 (a ∩ b⊥ ⊥ ) ≤ (a ∪ b⊥ )
27	26	df-le2 131	. . . . . . . . . . . 12 ((a ∩ b⊥ ⊥ ) ∪ (a ∪ b⊥ )) = (a ∪ b⊥ )
28	23, 27	ax-r2 36	. . . . . . . . . . 11 ((a ∪ b⊥ ) ∪ (a ∩ b⊥ ⊥ )) = (a ∪ b⊥ )
29		ax-a2 31	. . . . . . . . . . . 12 ((a ∪ b⊥ ⊥ ) ∪ (a ∩ b⊥ ⊥ )) = ((a ∩ b⊥ ⊥ ) ∪ (a ∪ b⊥ ⊥ ))
30		leo 158	. . . . . . . . . . . . . 14 a ≤ (a ∪ b⊥ ⊥ )
31	24, 30	letr 137	. . . . . . . . . . . . 13 (a ∩ b⊥ ⊥ ) ≤ (a ∪ b⊥ ⊥ )
32	31	df-le2 131	. . . . . . . . . . . 12 ((a ∩ b⊥ ⊥ ) ∪ (a ∪ b⊥ ⊥ )) = (a ∪ b⊥ ⊥ )
33	29, 32	ax-r2 36	. . . . . . . . . . 11 ((a ∪ b⊥ ⊥ ) ∪ (a ∩ b⊥ ⊥ )) = (a ∪ b⊥ ⊥ )
34	28, 33	2an 79	. . . . . . . . . 10 (((a ∪ b⊥ ) ∪ (a ∩ b⊥ ⊥ )) ∩ ((a ∪ b⊥ ⊥ ) ∪ (a ∩ b⊥ ⊥ ))) = ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))
35		id 59	. . . . . . . . . 10 ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) = ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))
36	34, 35	ax-r2 36	. . . . . . . . 9 (((a ∪ b⊥ ) ∪ (a ∩ b⊥ ⊥ )) ∩ ((a ∪ b⊥ ⊥ ) ∪ (a ∩ b⊥ ⊥ ))) = ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))
37	36	lan 77	. . . . . . . 8 ((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∩ (((a ∪ b⊥ ) ∪ (a ∩ b⊥ ⊥ )) ∩ ((a ∪ b⊥ ⊥ ) ∪ (a ∩ b⊥ ⊥ )))) = ((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∩ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )))
38		id 59	. . . . . . . 8 ((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∩ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))) = ((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∩ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )))
39	37, 38	ax-r2 36	. . . . . . 7 ((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∩ (((a ∪ b⊥ ) ∪ (a ∩ b⊥ ⊥ )) ∩ ((a ∪ b⊥ ⊥ ) ∪ (a ∩ b⊥ ⊥ )))) = ((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∩ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )))
40	22, 39	ax-r2 36	. . . . . 6 ((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∩ (((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) ∪ (a ∩ b⊥ ⊥ ))) = ((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∩ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )))
41	15, 40	ax-r2 36	. . . . 5 ((a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))) ∪ (a ∩ b⊥ ⊥ )) = ((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∩ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )))
42	8, 41	ax-r2 36	. . . 4 (((a →3 b⊥ )⊥ ∩ a⊥ ) ∪ ((a →3 b⊥ )⊥ ∩ a⊥ ⊥ )) = ((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∩ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )))
43		u3lemnona 667	. . . . . 6 ((a →3 b⊥ )⊥ ∪ a⊥ ) = (a⊥ ∪ (a ∩ b⊥ ⊥ ))
44	43	lan 77	. . . . 5 ((a →3 b⊥ ) ∩ ((a →3 b⊥ )⊥ ∪ a⊥ )) = ((a →3 b⊥ ) ∩ (a⊥ ∪ (a ∩ b⊥ ⊥ )))
45		comi31 508	. . . . . . . 8 a C (a →3 b⊥ )
46	45	comcom3 454	. . . . . . 7 a⊥ C (a →3 b⊥ )
47	46, 10	fh2 470	. . . . . 6 ((a →3 b⊥ ) ∩ (a⊥ ∪ (a ∩ b⊥ ⊥ ))) = (((a →3 b⊥ ) ∩ a⊥ ) ∪ ((a →3 b⊥ ) ∩ (a ∩ b⊥ ⊥ )))
48		u3lemana 607	. . . . . . . 8 ((a →3 b⊥ ) ∩ a⊥ ) = ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))
49		anandi 114	. . . . . . . . 9 ((a →3 b⊥ ) ∩ (a ∩ b⊥ ⊥ )) = (((a →3 b⊥ ) ∩ a) ∩ ((a →3 b⊥ ) ∩ b⊥ ⊥ ))
50		u3lemaa 602	. . . . . . . . . . 11 ((a →3 b⊥ ) ∩ a) = (a ∩ (a⊥ ∪ b⊥ ))
51		u3lemanb 617	. . . . . . . . . . 11 ((a →3 b⊥ ) ∩ b⊥ ⊥ ) = (a⊥ ∩ b⊥ ⊥ )
52	50, 51	2an 79	. . . . . . . . . 10 (((a →3 b⊥ ) ∩ a) ∩ ((a →3 b⊥ ) ∩ b⊥ ⊥ )) = ((a ∩ (a⊥ ∪ b⊥ )) ∩ (a⊥ ∩ b⊥ ⊥ ))
53		an4 86	. . . . . . . . . . 11 ((a ∩ (a⊥ ∪ b⊥ )) ∩ (a⊥ ∩ b⊥ ⊥ )) = ((a ∩ a⊥ ) ∩ ((a⊥ ∪ b⊥ ) ∩ b⊥ ⊥ ))
54		ancom 74	. . . . . . . . . . . 12 ((a ∩ a⊥ ) ∩ ((a⊥ ∪ b⊥ ) ∩ b⊥ ⊥ )) = (((a⊥ ∪ b⊥ ) ∩ b⊥ ⊥ ) ∩ (a ∩ a⊥ ))
55		dff 101	. . . . . . . . . . . . . . 15 0 = (a ∩ a⊥ )
56	55	ax-r1 35	. . . . . . . . . . . . . 14 (a ∩ a⊥ ) = 0
57	56	lan 77	. . . . . . . . . . . . 13 (((a⊥ ∪ b⊥ ) ∩ b⊥ ⊥ ) ∩ (a ∩ a⊥ )) = (((a⊥ ∪ b⊥ ) ∩ b⊥ ⊥ ) ∩ 0)
58		an0 108	. . . . . . . . . . . . 13 (((a⊥ ∪ b⊥ ) ∩ b⊥ ⊥ ) ∩ 0) = 0
59	57, 58	ax-r2 36	. . . . . . . . . . . 12 (((a⊥ ∪ b⊥ ) ∩ b⊥ ⊥ ) ∩ (a ∩ a⊥ )) = 0
60	54, 59	ax-r2 36	. . . . . . . . . . 11 ((a ∩ a⊥ ) ∩ ((a⊥ ∪ b⊥ ) ∩ b⊥ ⊥ )) = 0
61	53, 60	ax-r2 36	. . . . . . . . . 10 ((a ∩ (a⊥ ∪ b⊥ )) ∩ (a⊥ ∩ b⊥ ⊥ )) = 0
62	52, 61	ax-r2 36	. . . . . . . . 9 (((a →3 b⊥ ) ∩ a) ∩ ((a →3 b⊥ ) ∩ b⊥ ⊥ )) = 0
63	49, 62	ax-r2 36	. . . . . . . 8 ((a →3 b⊥ ) ∩ (a ∩ b⊥ ⊥ )) = 0
64	48, 63	2or 72	. . . . . . 7 (((a →3 b⊥ ) ∩ a⊥ ) ∪ ((a →3 b⊥ ) ∩ (a ∩ b⊥ ⊥ ))) = (((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )) ∪ 0)
65		or0 102	. . . . . . 7 (((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )) ∪ 0) = ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))
66	64, 65	ax-r2 36	. . . . . 6 (((a →3 b⊥ ) ∩ a⊥ ) ∪ ((a →3 b⊥ ) ∩ (a ∩ b⊥ ⊥ ))) = ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))
67	47, 66	ax-r2 36	. . . . 5 ((a →3 b⊥ ) ∩ (a⊥ ∪ (a ∩ b⊥ ⊥ ))) = ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))
68	44, 67	ax-r2 36	. . . 4 ((a →3 b⊥ ) ∩ ((a →3 b⊥ )⊥ ∪ a⊥ )) = ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))
69	42, 68	2or 72	. . 3 ((((a →3 b⊥ )⊥ ∩ a⊥ ) ∪ ((a →3 b⊥ )⊥ ∩ a⊥ ⊥ )) ∪ ((a →3 b⊥ ) ∩ ((a →3 b⊥ )⊥ ∪ a⊥ ))) = (((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∩ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )))
70		comanr1 464	. . . . . . . . 9 a⊥ C (a⊥ ∩ b⊥ )
71		comanr1 464	. . . . . . . . 9 a⊥ C (a⊥ ∩ b⊥ ⊥ )
72	70, 71	com2or 483	. . . . . . . 8 a⊥ C ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))
73	72	comcom 453	. . . . . . 7 ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )) C a⊥
74	73	comcom7 460	. . . . . . . 8 ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )) C a
75		comanr2 465	. . . . . . . . . . 11 b⊥ C (a⊥ ∩ b⊥ )
76	75	comcom3 454	. . . . . . . . . 10 b⊥ ⊥ C (a⊥ ∩ b⊥ )
77		comanr2 465	. . . . . . . . . 10 b⊥ ⊥ C (a⊥ ∩ b⊥ ⊥ )
78	76, 77	com2or 483	. . . . . . . . 9 b⊥ ⊥ C ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))
79	78	comcom 453	. . . . . . . 8 ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )) C b⊥ ⊥
80	74, 79	com2an 484	. . . . . . 7 ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )) C (a ∩ b⊥ ⊥ )
81	73, 80	com2or 483	. . . . . 6 ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )) C (a⊥ ∪ (a ∩ b⊥ ⊥ ))
82	81	comcom 453	. . . . 5 (a⊥ ∪ (a ∩ b⊥ ⊥ )) C ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))
83	13	comcom 453	. . . . . . . 8 ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) C a
84	83	comcom2 183	. . . . . . 7 ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) C a⊥
85		comorr2 463	. . . . . . . . . . 11 b⊥ C (a ∪ b⊥ )
86	85	comcom3 454	. . . . . . . . . 10 b⊥ ⊥ C (a ∪ b⊥ )
87		comorr2 463	. . . . . . . . . 10 b⊥ ⊥ C (a ∪ b⊥ ⊥ )
88	86, 87	com2an 484	. . . . . . . . 9 b⊥ ⊥ C ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))
89	88	comcom 453	. . . . . . . 8 ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) C b⊥ ⊥
90	83, 89	com2an 484	. . . . . . 7 ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) C (a ∩ b⊥ ⊥ )
91	84, 90	com2or 483	. . . . . 6 ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) C (a⊥ ∪ (a ∩ b⊥ ⊥ ))
92	91	comcom 453	. . . . 5 (a⊥ ∪ (a ∩ b⊥ ⊥ )) C ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))
93	82, 92	fh4r 476	. . . 4 (((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∩ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))) = (((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))) ∩ (((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))))
94		ax-a2 31	. . . . . . 7 ((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))) = (((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )) ∪ (a⊥ ∪ (a ∩ b⊥ ⊥ )))
95		lea 160	. . . . . . . . . . 11 (a⊥ ∩ b⊥ ) ≤ a⊥
96		lea 160	. . . . . . . . . . 11 (a⊥ ∩ b⊥ ⊥ ) ≤ a⊥
97	95, 96	lel2or 170	. . . . . . . . . 10 ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )) ≤ a⊥
98		leo 158	. . . . . . . . . 10 a⊥ ≤ (a⊥ ∪ (a ∩ b⊥ ⊥ ))
99	97, 98	letr 137	. . . . . . . . 9 ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )) ≤ (a⊥ ∪ (a ∩ b⊥ ⊥ ))
100	99	df-le2 131	. . . . . . . 8 (((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )) ∪ (a⊥ ∪ (a ∩ b⊥ ⊥ ))) = (a⊥ ∪ (a ∩ b⊥ ⊥ ))
101		id 59	. . . . . . . 8 (a⊥ ∪ (a ∩ b⊥ ⊥ )) = (a⊥ ∪ (a ∩ b⊥ ⊥ ))
102	100, 101	ax-r2 36	. . . . . . 7 (((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )) ∪ (a⊥ ∪ (a ∩ b⊥ ⊥ ))) = (a⊥ ∪ (a ∩ b⊥ ⊥ ))
103	94, 102	ax-r2 36	. . . . . 6 ((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))) = (a⊥ ∪ (a ∩ b⊥ ⊥ ))
104		ax-a2 31	. . . . . . . . 9 ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )) = ((a⊥ ∩ b⊥ ⊥ ) ∪ (a⊥ ∩ b⊥ ))
105		anor3 90	. . . . . . . . . . 11 (a⊥ ∩ b⊥ ⊥ ) = (a ∪ b⊥ )⊥
106		anor2 89	. . . . . . . . . . 11 (a⊥ ∩ b⊥ ) = (a ∪ b⊥ ⊥ )⊥
107	105, 106	2or 72	. . . . . . . . . 10 ((a⊥ ∩ b⊥ ⊥ ) ∪ (a⊥ ∩ b⊥ )) = ((a ∪ b⊥ )⊥ ∪ (a ∪ b⊥ ⊥ )⊥ )
108		oran3 93	. . . . . . . . . 10 ((a ∪ b⊥ )⊥ ∪ (a ∪ b⊥ ⊥ )⊥ ) = ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))⊥
109	107, 108	ax-r2 36	. . . . . . . . 9 ((a⊥ ∩ b⊥ ⊥ ) ∪ (a⊥ ∩ b⊥ )) = ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))⊥
110	104, 109	ax-r2 36	. . . . . . . 8 ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )) = ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))⊥
111	110	lor 70	. . . . . . 7 (((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))) = (((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) ∪ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))⊥ )
112		df-t 41	. . . . . . . 8 1 = (((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) ∪ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))⊥ )
113	112	ax-r1 35	. . . . . . 7 (((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) ∪ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))⊥ ) = 1
114	111, 113	ax-r2 36	. . . . . 6 (((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))) = 1
115	103, 114	2an 79	. . . . 5 (((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))) ∩ (((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )))) = ((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∩ 1)
116		an1 106	. . . . . 6 ((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∩ 1) = (a⊥ ∪ (a ∩ b⊥ ⊥ ))
117		df-i1 44	. . . . . . . 8 (a →1 b⊥ ⊥ ) = (a⊥ ∪ (a ∩ b⊥ ⊥ ))
118	117	ax-r1 35	. . . . . . 7 (a⊥ ∪ (a ∩ b⊥ ⊥ )) = (a →1 b⊥ ⊥ )
119		ax-a1 30	. . . . . . . . 9 b = b⊥ ⊥
120	119	ax-r1 35	. . . . . . . 8 b⊥ ⊥ = b
121	120	ud1lem0a 255	. . . . . . 7 (a →1 b⊥ ⊥ ) = (a →1 b)
122	118, 121	ax-r2 36	. . . . . 6 (a⊥ ∪ (a ∩ b⊥ ⊥ )) = (a →1 b)
123	116, 122	ax-r2 36	. . . . 5 ((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∩ 1) = (a →1 b)
124	115, 123	ax-r2 36	. . . 4 (((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))) ∩ (((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )))) = (a →1 b)
125	93, 124	ax-r2 36	. . 3 (((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∩ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))) = (a →1 b)
126	69, 125	ax-r2 36	. 2 ((((a →3 b⊥ )⊥ ∩ a⊥ ) ∪ ((a →3 b⊥ )⊥ ∩ a⊥ ⊥ )) ∪ ((a →3 b⊥ ) ∩ ((a →3 b⊥ )⊥ ∪ a⊥ ))) = (a →1 b)
127	1, 126	ax-r2 36	1 ((a →3 b⊥ ) →3 a⊥ ) = (a →1 b)

This proof depends on syntax axioms:   = wb 1  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  1wt 8  0wf 9   →₁ wi1 12   →₃ wi3 14

This proof depends on axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a4 33  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-r3 439

This proof depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i1 44  df-i3 46  df-le1 130  df-le2 131  df-c1 132  df-c2 133

This theorem is used by:  u3lem14a  791  u3lem14aa2  793