Theorem xxdp15 1202

Description: Part of proof (1)=>(5) in Day/Pickering 1982. (Contributed by NM, 11-Apr-2012.)

Hypotheses

Ref	Expression
xxdp.1	p2 ≤ (a2 ∪ b2)
xxdp.c0	c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))
xxdp.c1	c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))
xxdp.c2	c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))
xxdp.d	d = (a2 ∪ (a0 ∩ (a1 ∪ b1)))
xxdp.e	e = (b0 ∩ (a0 ∪ p0))
xxdp.p	p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))
xxdp.p0	p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))
xxdp.p2	p2 = ((a0 ∪ b0) ∩ (a1 ∪ b1))

Assertion

Ref	Expression
xxdp15	((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ ((c0 ∪ c1) ∪ (b1 ∩ (a0 ∪ a1)))

Proof of Theorem xxdp15

Step	Hyp	Ref	Expression
1		xxdp.e	. . . . . . . . . . 11 e = (b0 ∩ (a0 ∪ p0))
2		xxdp.p0	. . . . . . . . . . . . 13 p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))
3	2	lor 70	. . . . . . . . . . . 12 (a0 ∪ p0) = (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2)))
4	3	lan 77	. . . . . . . . . . 11 (b0 ∩ (a0 ∪ p0)) = (b0 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2))))
5	1, 4	tr 62	. . . . . . . . . 10 e = (b0 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2))))
6	5	lor 70	. . . . . . . . 9 (a0 ∪ e) = (a0 ∪ (b0 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2)))))
7	6	ran 78	. . . . . . . 8 ((a0 ∪ e) ∩ (a1 ∪ b1)) = ((a0 ∪ (b0 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2))))) ∩ (a1 ∪ b1))
8		le1 146	. . . . . . . . . . . 12 b0 ≤ 1
9	8	leran 153	. . . . . . . . . . 11 (b0 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2)))) ≤ (1 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2))))
10	9	lelor 166	. . . . . . . . . 10 (a0 ∪ (b0 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2))))) ≤ (a0 ∪ (1 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2)))))
11	10	leran 153	. . . . . . . . 9 ((a0 ∪ (b0 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2))))) ∩ (a1 ∪ b1)) ≤ ((a0 ∪ (1 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2))))) ∩ (a1 ∪ b1))
12		an1r 107	. . . . . . . . . . . . . . 15 (1 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2)))) = (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2)))
13	12	lor 70	. . . . . . . . . . . . . 14 (a0 ∪ (1 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2))))) = (a0 ∪ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2))))
14		orass 75	. . . . . . . . . . . . . . 15 ((a0 ∪ a0) ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2))) = (a0 ∪ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2))))
15	14	cm 61	. . . . . . . . . . . . . 14 (a0 ∪ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2)))) = ((a0 ∪ a0) ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2)))
16		oridm 110	. . . . . . . . . . . . . . . 16 (a0 ∪ a0) = a0
17	16	ror 71	. . . . . . . . . . . . . . 15 ((a0 ∪ a0) ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2))) = (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2)))
18		orcom 73	. . . . . . . . . . . . . . 15 (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2))) = (((a1 ∪ b1) ∩ (a2 ∪ b2)) ∪ a0)
19	17, 18	tr 62	. . . . . . . . . . . . . 14 ((a0 ∪ a0) ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2))) = (((a1 ∪ b1) ∩ (a2 ∪ b2)) ∪ a0)
20	13, 15, 19	3tr 65	. . . . . . . . . . . . 13 (a0 ∪ (1 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2))))) = (((a1 ∪ b1) ∩ (a2 ∪ b2)) ∪ a0)
21	20	ran 78	. . . . . . . . . . . 12 ((a0 ∪ (1 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2))))) ∩ (a1 ∪ b1)) = ((((a1 ∪ b1) ∩ (a2 ∪ b2)) ∪ a0) ∩ (a1 ∪ b1))
22		lea 160	. . . . . . . . . . . . 13 ((a1 ∪ b1) ∩ (a2 ∪ b2)) ≤ (a1 ∪ b1)
23	22	mlduali 1128	. . . . . . . . . . . 12 ((((a1 ∪ b1) ∩ (a2 ∪ b2)) ∪ a0) ∩ (a1 ∪ b1)) = (((a1 ∪ b1) ∩ (a2 ∪ b2)) ∪ (a0 ∩ (a1 ∪ b1)))
24	21, 23	tr 62	. . . . . . . . . . 11 ((a0 ∪ (1 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2))))) ∩ (a1 ∪ b1)) = (((a1 ∪ b1) ∩ (a2 ∪ b2)) ∪ (a0 ∩ (a1 ∪ b1)))
25		lear 161	. . . . . . . . . . . 12 ((a1 ∪ b1) ∩ (a2 ∪ b2)) ≤ (a2 ∪ b2)
26	25	leror 152	. . . . . . . . . . 11 (((a1 ∪ b1) ∩ (a2 ∪ b2)) ∪ (a0 ∩ (a1 ∪ b1))) ≤ ((a2 ∪ b2) ∪ (a0 ∩ (a1 ∪ b1)))
27	24, 26	bltr 138	. . . . . . . . . 10 ((a0 ∪ (1 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2))))) ∩ (a1 ∪ b1)) ≤ ((a2 ∪ b2) ∪ (a0 ∩ (a1 ∪ b1)))
28		or32 82	. . . . . . . . . . 11 ((a2 ∪ b2) ∪ (a0 ∩ (a1 ∪ b1))) = ((a2 ∪ (a0 ∩ (a1 ∪ b1))) ∪ b2)
29		xxdp.d	. . . . . . . . . . . . 13 d = (a2 ∪ (a0 ∩ (a1 ∪ b1)))
30	29	ror 71	. . . . . . . . . . . 12 (d ∪ b2) = ((a2 ∪ (a0 ∩ (a1 ∪ b1))) ∪ b2)
31	30	cm 61	. . . . . . . . . . 11 ((a2 ∪ (a0 ∩ (a1 ∪ b1))) ∪ b2) = (d ∪ b2)
32	28, 31	tr 62	. . . . . . . . . 10 ((a2 ∪ b2) ∪ (a0 ∩ (a1 ∪ b1))) = (d ∪ b2)
33	27, 32	lbtr 139	. . . . . . . . 9 ((a0 ∪ (1 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2))))) ∩ (a1 ∪ b1)) ≤ (d ∪ b2)
34	11, 33	letr 137	. . . . . . . 8 ((a0 ∪ (b0 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2))))) ∩ (a1 ∪ b1)) ≤ (d ∪ b2)
35	7, 34	bltr 138	. . . . . . 7 ((a0 ∪ e) ∩ (a1 ∪ b1)) ≤ (d ∪ b2)
36	35	ax-arg 1153	. . . . . 6 ((a0 ∪ a1) ∩ (e ∪ b1)) ≤ (((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2)))
37	1	ror 71	. . . . . . 7 (e ∪ b1) = ((b0 ∩ (a0 ∪ p0)) ∪ b1)
38	37	lan 77	. . . . . 6 ((a0 ∪ a1) ∩ (e ∪ b1)) = ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1))
39	29	lor 70	. . . . . . . 8 (a0 ∪ d) = (a0 ∪ (a2 ∪ (a0 ∩ (a1 ∪ b1))))
40	1	ror 71	. . . . . . . 8 (e ∪ b2) = ((b0 ∩ (a0 ∪ p0)) ∪ b2)
41	39, 40	2an 79	. . . . . . 7 ((a0 ∪ d) ∩ (e ∪ b2)) = ((a0 ∪ (a2 ∪ (a0 ∩ (a1 ∪ b1)))) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b2))
42	29	lor 70	. . . . . . . 8 (a1 ∪ d) = (a1 ∪ (a2 ∪ (a0 ∩ (a1 ∪ b1))))
43	42	ran 78	. . . . . . 7 ((a1 ∪ d) ∩ (b1 ∪ b2)) = ((a1 ∪ (a2 ∪ (a0 ∩ (a1 ∪ b1)))) ∩ (b1 ∪ b2))
44	41, 43	2or 72	. . . . . 6 (((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2))) = (((a0 ∪ (a2 ∪ (a0 ∩ (a1 ∪ b1)))) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b2)) ∪ ((a1 ∪ (a2 ∪ (a0 ∩ (a1 ∪ b1)))) ∩ (b1 ∪ b2)))
45	36, 38, 44	le3tr2 141	. . . . 5 ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ (((a0 ∪ (a2 ∪ (a0 ∩ (a1 ∪ b1)))) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b2)) ∪ ((a1 ∪ (a2 ∪ (a0 ∩ (a1 ∪ b1)))) ∩ (b1 ∪ b2)))
46		or12 80	. . . . . . . 8 (a0 ∪ (a2 ∪ (a0 ∩ (a1 ∪ b1)))) = (a2 ∪ (a0 ∪ (a0 ∩ (a1 ∪ b1))))
47		orabs 120	. . . . . . . . 9 (a0 ∪ (a0 ∩ (a1 ∪ b1))) = a0
48	47	lor 70	. . . . . . . 8 (a2 ∪ (a0 ∪ (a0 ∩ (a1 ∪ b1)))) = (a2 ∪ a0)
49		orcom 73	. . . . . . . 8 (a2 ∪ a0) = (a0 ∪ a2)
50	46, 48, 49	3tr 65	. . . . . . 7 (a0 ∪ (a2 ∪ (a0 ∩ (a1 ∪ b1)))) = (a0 ∪ a2)
51	50	ran 78	. . . . . 6 ((a0 ∪ (a2 ∪ (a0 ∩ (a1 ∪ b1)))) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b2)) = ((a0 ∪ a2) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b2))
52		orass 75	. . . . . . . 8 ((a1 ∪ a2) ∪ (a0 ∩ (a1 ∪ b1))) = (a1 ∪ (a2 ∪ (a0 ∩ (a1 ∪ b1))))
53	52	ran 78	. . . . . . 7 (((a1 ∪ a2) ∪ (a0 ∩ (a1 ∪ b1))) ∩ (b1 ∪ b2)) = ((a1 ∪ (a2 ∪ (a0 ∩ (a1 ∪ b1)))) ∩ (b1 ∪ b2))
54	53	cm 61	. . . . . 6 ((a1 ∪ (a2 ∪ (a0 ∩ (a1 ∪ b1)))) ∩ (b1 ∪ b2)) = (((a1 ∪ a2) ∪ (a0 ∩ (a1 ∪ b1))) ∩ (b1 ∪ b2))
55	51, 54	2or 72	. . . . 5 (((a0 ∪ (a2 ∪ (a0 ∩ (a1 ∪ b1)))) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b2)) ∪ ((a1 ∪ (a2 ∪ (a0 ∩ (a1 ∪ b1)))) ∩ (b1 ∪ b2))) = (((a0 ∪ a2) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b2)) ∪ (((a1 ∪ a2) ∪ (a0 ∩ (a1 ∪ b1))) ∩ (b1 ∪ b2)))
56	45, 55	lbtr 139	. . . 4 ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ (((a0 ∪ a2) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b2)) ∪ (((a1 ∪ a2) ∪ (a0 ∩ (a1 ∪ b1))) ∩ (b1 ∪ b2)))
57		ax-a2 31	. . . . . . . . . 10 (a1 ∪ a2) = (a2 ∪ a1)
58		ax-a2 31	. . . . . . . . . . 11 (a1 ∪ b1) = (b1 ∪ a1)
59	58	lan 77	. . . . . . . . . 10 (a0 ∩ (a1 ∪ b1)) = (a0 ∩ (b1 ∪ a1))
60	57, 59	2or 72	. . . . . . . . 9 ((a1 ∪ a2) ∪ (a0 ∩ (a1 ∪ b1))) = ((a2 ∪ a1) ∪ (a0 ∩ (b1 ∪ a1)))
61		orass 75	. . . . . . . . 9 ((a2 ∪ a1) ∪ (a0 ∩ (b1 ∪ a1))) = (a2 ∪ (a1 ∪ (a0 ∩ (b1 ∪ a1))))
62	60, 61	tr 62	. . . . . . . 8 ((a1 ∪ a2) ∪ (a0 ∩ (a1 ∪ b1))) = (a2 ∪ (a1 ∪ (a0 ∩ (b1 ∪ a1))))
63		ml3le 1129	. . . . . . . . 9 (a1 ∪ (a0 ∩ (b1 ∪ a1))) ≤ (a1 ∪ (b1 ∩ (a0 ∪ a1)))
64	63	lelor 166	. . . . . . . 8 (a2 ∪ (a1 ∪ (a0 ∩ (b1 ∪ a1)))) ≤ (a2 ∪ (a1 ∪ (b1 ∩ (a0 ∪ a1))))
65	62, 64	bltr 138	. . . . . . 7 ((a1 ∪ a2) ∪ (a0 ∩ (a1 ∪ b1))) ≤ (a2 ∪ (a1 ∪ (b1 ∩ (a0 ∪ a1))))
66		orass 75	. . . . . . . . 9 ((a2 ∪ a1) ∪ (b1 ∩ (a0 ∪ a1))) = (a2 ∪ (a1 ∪ (b1 ∩ (a0 ∪ a1))))
67	66	cm 61	. . . . . . . 8 (a2 ∪ (a1 ∪ (b1 ∩ (a0 ∪ a1)))) = ((a2 ∪ a1) ∪ (b1 ∩ (a0 ∪ a1)))
68		ax-a2 31	. . . . . . . . 9 (a2 ∪ a1) = (a1 ∪ a2)
69	68	ror 71	. . . . . . . 8 ((a2 ∪ a1) ∪ (b1 ∩ (a0 ∪ a1))) = ((a1 ∪ a2) ∪ (b1 ∩ (a0 ∪ a1)))
70	67, 69	tr 62	. . . . . . 7 (a2 ∪ (a1 ∪ (b1 ∩ (a0 ∪ a1)))) = ((a1 ∪ a2) ∪ (b1 ∩ (a0 ∪ a1)))
71	65, 70	lbtr 139	. . . . . 6 ((a1 ∪ a2) ∪ (a0 ∩ (a1 ∪ b1))) ≤ ((a1 ∪ a2) ∪ (b1 ∩ (a0 ∪ a1)))
72	71	leran 153	. . . . 5 (((a1 ∪ a2) ∪ (a0 ∩ (a1 ∪ b1))) ∩ (b1 ∪ b2)) ≤ (((a1 ∪ a2) ∪ (b1 ∩ (a0 ∪ a1))) ∩ (b1 ∪ b2))
73	72	lelor 166	. . . 4 (((a0 ∪ a2) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b2)) ∪ (((a1 ∪ a2) ∪ (a0 ∩ (a1 ∪ b1))) ∩ (b1 ∪ b2))) ≤ (((a0 ∪ a2) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b2)) ∪ (((a1 ∪ a2) ∪ (b1 ∩ (a0 ∪ a1))) ∩ (b1 ∪ b2)))
74	56, 73	letr 137	. . 3 ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ (((a0 ∪ a2) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b2)) ∪ (((a1 ∪ a2) ∪ (b1 ∩ (a0 ∪ a1))) ∩ (b1 ∪ b2)))
75		lea 160	. . . . . . 7 (b0 ∩ (a0 ∪ p0)) ≤ b0
76	75	leror 152	. . . . . 6 ((b0 ∩ (a0 ∪ p0)) ∪ b2) ≤ (b0 ∪ b2)
77	76	lelan 167	. . . . 5 ((a0 ∪ a2) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b2)) ≤ ((a0 ∪ a2) ∩ (b0 ∪ b2))
78		leao1 162	. . . . . . . 8 (b1 ∩ (a0 ∪ a1)) ≤ (b1 ∪ b2)
79	78	mldual2i 1127	. . . . . . 7 ((b1 ∪ b2) ∩ ((a1 ∪ a2) ∪ (b1 ∩ (a0 ∪ a1)))) = (((b1 ∪ b2) ∩ (a1 ∪ a2)) ∪ (b1 ∩ (a0 ∪ a1)))
80		ancom 74	. . . . . . 7 ((b1 ∪ b2) ∩ ((a1 ∪ a2) ∪ (b1 ∩ (a0 ∪ a1)))) = (((a1 ∪ a2) ∪ (b1 ∩ (a0 ∪ a1))) ∩ (b1 ∪ b2))
81		ancom 74	. . . . . . . 8 ((b1 ∪ b2) ∩ (a1 ∪ a2)) = ((a1 ∪ a2) ∩ (b1 ∪ b2))
82	81	ror 71	. . . . . . 7 (((b1 ∪ b2) ∩ (a1 ∪ a2)) ∪ (b1 ∩ (a0 ∪ a1))) = (((a1 ∪ a2) ∩ (b1 ∪ b2)) ∪ (b1 ∩ (a0 ∪ a1)))
83	79, 80, 82	3tr2 64	. . . . . 6 (((a1 ∪ a2) ∪ (b1 ∩ (a0 ∪ a1))) ∩ (b1 ∪ b2)) = (((a1 ∪ a2) ∩ (b1 ∪ b2)) ∪ (b1 ∩ (a0 ∪ a1)))
84	83	bile 142	. . . . 5 (((a1 ∪ a2) ∪ (b1 ∩ (a0 ∪ a1))) ∩ (b1 ∪ b2)) ≤ (((a1 ∪ a2) ∩ (b1 ∪ b2)) ∪ (b1 ∩ (a0 ∪ a1)))
85	77, 84	le2or 168	. . . 4 (((a0 ∪ a2) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b2)) ∪ (((a1 ∪ a2) ∪ (b1 ∩ (a0 ∪ a1))) ∩ (b1 ∪ b2))) ≤ (((a0 ∪ a2) ∩ (b0 ∪ b2)) ∪ (((a1 ∪ a2) ∩ (b1 ∪ b2)) ∪ (b1 ∩ (a0 ∪ a1))))
86		or12 80	. . . 4 (((a0 ∪ a2) ∩ (b0 ∪ b2)) ∪ (((a1 ∪ a2) ∩ (b1 ∪ b2)) ∪ (b1 ∩ (a0 ∪ a1)))) = (((a1 ∪ a2) ∩ (b1 ∪ b2)) ∪ (((a0 ∪ a2) ∩ (b0 ∪ b2)) ∪ (b1 ∩ (a0 ∪ a1))))
87	85, 86	lbtr 139	. . 3 (((a0 ∪ a2) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b2)) ∪ (((a1 ∪ a2) ∪ (b1 ∩ (a0 ∪ a1))) ∩ (b1 ∪ b2))) ≤ (((a1 ∪ a2) ∩ (b1 ∪ b2)) ∪ (((a0 ∪ a2) ∩ (b0 ∪ b2)) ∪ (b1 ∩ (a0 ∪ a1))))
88	74, 87	letr 137	. 2 ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ (((a1 ∪ a2) ∩ (b1 ∪ b2)) ∪ (((a0 ∪ a2) ∩ (b0 ∪ b2)) ∪ (b1 ∩ (a0 ∪ a1))))
89		xxdp.c0	. . . . 5 c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))
90		xxdp.c1	. . . . . 6 c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))
91	90	ror 71	. . . . 5 (c1 ∪ (b1 ∩ (a0 ∪ a1))) = (((a0 ∪ a2) ∩ (b0 ∪ b2)) ∪ (b1 ∩ (a0 ∪ a1)))
92	89, 91	2or 72	. . . 4 (c0 ∪ (c1 ∪ (b1 ∩ (a0 ∪ a1)))) = (((a1 ∪ a2) ∩ (b1 ∪ b2)) ∪ (((a0 ∪ a2) ∩ (b0 ∪ b2)) ∪ (b1 ∩ (a0 ∪ a1))))
93	92	cm 61	. . 3 (((a1 ∪ a2) ∩ (b1 ∪ b2)) ∪ (((a0 ∪ a2) ∩ (b0 ∪ b2)) ∪ (b1 ∩ (a0 ∪ a1)))) = (c0 ∪ (c1 ∪ (b1 ∩ (a0 ∪ a1))))
94		orass 75	. . . 4 ((c0 ∪ c1) ∪ (b1 ∩ (a0 ∪ a1))) = (c0 ∪ (c1 ∪ (b1 ∩ (a0 ∪ a1))))
95	94	cm 61	. . 3 (c0 ∪ (c1 ∪ (b1 ∩ (a0 ∪ a1)))) = ((c0 ∪ c1) ∪ (b1 ∩ (a0 ∪ a1)))
96	93, 95	tr 62	. 2 (((a1 ∪ a2) ∩ (b1 ∪ b2)) ∪ (((a0 ∪ a2) ∩ (b0 ∪ b2)) ∪ (b1 ∩ (a0 ∪ a1)))) = ((c0 ∪ c1) ∪ (b1 ∩ (a0 ∪ a1)))
97	88, 96	lbtr 139	1 ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ ((c0 ∪ c1) ∪ (b1 ∩ (a0 ∪ a1)))

Syntax hints:   = wb 1   ≤ wle 2   ∪ wo 6   ∩ wa 7  1wt 8

This theorem was proved from 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-ml 1122  ax-arg 1153

This theorem depends on definitions:  df-a 40  df-t 41  df-f 42  df-le1 130  df-le2 131

This theorem is referenced by: (None)