Theorem ledi 166

Description: Half of distributive law.

Assertion

Ref	Expression
ledi	((a ^ b) v (a ^ c)) =< (a ^ (b v c))

Proof of Theorem ledi

Step	Hyp	Ref	Expression
1		anidm 103	. . 3 (((a ^ b) v (a ^ c)) ^ ((a ^ b) v (a ^ c))) = ((a ^ b) v (a ^ c))
2	1	ax-r1 34	. 2 ((a ^ b) v (a ^ c)) = (((a ^ b) v (a ^ c)) ^ ((a ^ b) v (a ^ c)))
3		lea 152	. . . . 5 (a ^ b) =< a
4		lea 152	. . . . 5 (a ^ c) =< a
5	3, 4	le2or 160	. . . 4 ((a ^ b) v (a ^ c)) =< (a v a)
6		oridm 102	. . . 4 (a v a) = a
7	5, 6	lbtr 131	. . 3 ((a ^ b) v (a ^ c)) =< a
8		ancom 68	. . . . 5 (a ^ b) = (b ^ a)
9		lea 152	. . . . 5 (b ^ a) =< b
10	8, 9	bltr 130	. . . 4 (a ^ b) =< b
11		ancom 68	. . . . 5 (a ^ c) = (c ^ a)
12		lea 152	. . . . 5 (c ^ a) =< c
13	11, 12	bltr 130	. . . 4 (a ^ c) =< c
14	10, 13	le2or 160	. . 3 ((a ^ b) v (a ^ c)) =< (b v c)
15	7, 14	le2an 161	. 2 (((a ^ b) v (a ^ c)) ^ ((a ^ b) v (a ^ c))) =< (a ^ (b v c))
16	2, 15	bltr 130	1 ((a ^ b) v (a ^ c)) =< (a ^ (b v c))

Syntax hints:   =< wle 2   v wo 6   ^ wa 7

This theorem is referenced by:  ledir 167  distlem 180  wwfh1 208  wwfh2 209  ska2 414  fh1 451  fh2 452  i3orlem2 535  distid 869  oadist 999  oadistb 1000  oadistc 1002  oadistd 1003  4oadist 1023

This theorem was proved from axioms:  ax-a1 29  ax-a2 30  ax-a3 31  ax-a5 33  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37

This theorem depends on definitions:  df-a 39  df-t 40  df-f 41  df-le1 122  df-le2 123

metamath.org