Theorem l42modlem1 1149

Description: Lemma for l42mod 1151. (Contributed by NM, 8-Apr-2012.)

Assertion

Ref	Expression
l42modlem1	(((a ∪ b) ∪ d) ∩ ((a ∪ b) ∪ e)) = ((a ∪ b) ∪ ((a ∪ d) ∩ (b ∪ e)))

Proof of Theorem l42modlem1

Step	Hyp	Ref	Expression
1		leo 158	. . . . . 6 b ≤ (b ∪ e)
2	1	ml2i 1125	. . . . 5 (b ∪ ((a ∪ d) ∩ (b ∪ e))) = ((b ∪ (a ∪ d)) ∩ (b ∪ e))
3		ancom 74	. . . . 5 ((b ∪ (a ∪ d)) ∩ (b ∪ e)) = ((b ∪ e) ∩ (b ∪ (a ∪ d)))
4	2, 3	tr 62	. . . 4 (b ∪ ((a ∪ d) ∩ (b ∪ e))) = ((b ∪ e) ∩ (b ∪ (a ∪ d)))
5	4	lor 70	. . 3 (a ∪ (b ∪ ((a ∪ d) ∩ (b ∪ e)))) = (a ∪ ((b ∪ e) ∩ (b ∪ (a ∪ d))))
6	5	cm 61	. 2 (a ∪ ((b ∪ e) ∩ (b ∪ (a ∪ d)))) = (a ∪ (b ∪ ((a ∪ d) ∩ (b ∪ e))))
7		orass 75	. . . . 5 ((a ∪ b) ∪ d) = (a ∪ (b ∪ d))
8		or12 80	. . . . 5 (a ∪ (b ∪ d)) = (b ∪ (a ∪ d))
9	7, 8	tr 62	. . . 4 ((a ∪ b) ∪ d) = (b ∪ (a ∪ d))
10		orass 75	. . . 4 ((a ∪ b) ∪ e) = (a ∪ (b ∪ e))
11	9, 10	2an 79	. . 3 (((a ∪ b) ∪ d) ∩ ((a ∪ b) ∪ e)) = ((b ∪ (a ∪ d)) ∩ (a ∪ (b ∪ e)))
12		ancom 74	. . 3 ((b ∪ (a ∪ d)) ∩ (a ∪ (b ∪ e))) = ((a ∪ (b ∪ e)) ∩ (b ∪ (a ∪ d)))
13		leo 158	. . . . . 6 a ≤ (a ∪ d)
14	13	lerr 150	. . . . 5 a ≤ (b ∪ (a ∪ d))
15	14	ml2i 1125	. . . 4 (a ∪ ((b ∪ e) ∩ (b ∪ (a ∪ d)))) = ((a ∪ (b ∪ e)) ∩ (b ∪ (a ∪ d)))
16	15	cm 61	. . 3 ((a ∪ (b ∪ e)) ∩ (b ∪ (a ∪ d))) = (a ∪ ((b ∪ e) ∩ (b ∪ (a ∪ d))))
17	11, 12, 16	3tr 65	. 2 (((a ∪ b) ∪ d) ∩ ((a ∪ b) ∪ e)) = (a ∪ ((b ∪ e) ∩ (b ∪ (a ∪ d))))
18		orass 75	. 2 ((a ∪ b) ∪ ((a ∪ d) ∩ (b ∪ e))) = (a ∪ (b ∪ ((a ∪ d) ∩ (b ∪ e))))
19	6, 17, 18	3tr1 63	1 (((a ∪ b) ∪ d) ∩ ((a ∪ b) ∪ e)) = ((a ∪ b) ∪ ((a ∪ d) ∩ (b ∪ e)))

This proof depends on syntax axioms:   = wb 1   ∪ wo 6   ∩ wa 7

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

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

This theorem is used by:  l42mod  1151  testmod2  1215  testmod2expanded  1216