Theorem ledi 174

Description: Half of distributive law. (Contributed by NM, 28-Aug-1997.)

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))

This proof depends on syntax axioms:   ≤ wle 2   ∪ 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

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:  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  1044