Proof of Theorem anorabs2
Step | Hyp | Ref
| Expression |
1 | | lea 160 |
. . 3
(a ∩ (b ∪ (a ∩
(b ∪ c)))) ≤ a |
2 | | lear 161 |
. . . 4
(a ∩ (b ∪ (a ∩
(b ∪ c)))) ≤ (b
∪ (a ∩ (b ∪ c))) |
3 | | leo 158 |
. . . . 5
b ≤ (b ∪ c) |
4 | | lear 161 |
. . . . 5
(a ∩ (b ∪ c)) ≤
(b ∪ c) |
5 | 3, 4 | lel2or 170 |
. . . 4
(b ∪ (a ∩ (b ∪
c))) ≤ (b ∪ c) |
6 | 2, 5 | letr 137 |
. . 3
(a ∩ (b ∪ (a ∩
(b ∪ c)))) ≤ (b
∪ c) |
7 | 1, 6 | ler2an 173 |
. 2
(a ∩ (b ∪ (a ∩
(b ∪ c)))) ≤ (a
∩ (b ∪ c)) |
8 | | lea 160 |
. . 3
(a ∩ (b ∪ c)) ≤
a |
9 | | leor 159 |
. . 3
(a ∩ (b ∪ c)) ≤
(b ∪ (a ∩ (b ∪
c))) |
10 | 8, 9 | ler2an 173 |
. 2
(a ∩ (b ∪ c)) ≤
(a ∩ (b ∪ (a ∩
(b ∪ c)))) |
11 | 7, 10 | lebi 145 |
1
(a ∩ (b ∪ (a ∩
(b ∪ c)))) = (a ∩
(b ∪ c)) |