Theorem ledi 174

Description: Half of distributive law.

Assertion

Ref	Expression
ledi	((a ∩ b) ∪ (a ∩ c)) ≤ (a ∩ (b ∪ c))

Proof of Theorem ledi

Step	Hyp	Ref	Expression
1		anidm 111	. . 3 (((a ∩ b) ∪ (a ∩ c)) ∩ ((a ∩ b) ∪ (a ∩ c))) = ((a ∩ b) ∪ (a ∩ c))
2	1	ax-r1 35	. 2 ((a ∩ b) ∪ (a ∩ c)) = (((a ∩ b) ∪ (a ∩ c)) ∩ ((a ∩ b) ∪ (a ∩ c)))
3		lea 160	. . . . 5 (a ∩ b) ≤ a
4		lea 160	. . . . 5 (a ∩ c) ≤ a
5	3, 4	le2or 168	. . . 4 ((a ∩ b) ∪ (a ∩ c)) ≤ (a ∪ a)
6		oridm 110	. . . 4 (a ∪ a) = a
7	5, 6	lbtr 139	. . 3 ((a ∩ b) ∪ (a ∩ c)) ≤ a
8		ancom 74	. . . . 5 (a ∩ b) = (b ∩ a)
9		lea 160	. . . . 5 (b ∩ a) ≤ b
10	8, 9	bltr 138	. . . 4 (a ∩ b) ≤ b
11		ancom 74	. . . . 5 (a ∩ c) = (c ∩ a)
12		lea 160	. . . . 5 (c ∩ a) ≤ c
13	11, 12	bltr 138	. . . 4 (a ∩ c) ≤ c
14	10, 13	le2or 168	. . 3 ((a ∩ b) ∪ (a ∩ c)) ≤ (b ∪ c)
15	7, 14	le2an 169	. 2 (((a ∩ b) ∪ (a ∩ c)) ∩ ((a ∩ b) ∪ (a ∩ c))) ≤ (a ∩ (b ∪ c))
16	2, 15	bltr 138	1 ((a ∩ b) ∪ (a ∩ c)) ≤ (a ∩ (b ∪ c))

Syntax hints:   ≤ wle 2   ∪ wo 6   ∩ wa 7

This theorem is referenced by:  ledir 175  distlem 188  wwfh1 216  wwfh2 217  ska2 432  fh1 469  fh2 470  i3orlem2 553  distid 887  oadist 1019  oadistb 1020  oadistc 1022  oadistd 1023  4oadist 1043

This theorem was proved from 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

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

Copyright terms: Public domain