Theorem leao4 165

Description: L.e. absorption. (Contributed by NM, 8-Jul-2000.)

Assertion

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

Proof of Theorem leao4

Step	Hyp	Ref	Expression
1		lear 161	. 2 (b ∩ a) ≤ a
2		leor 159	. 2 a ≤ (c ∪ a)
3	1, 2	letr 137	1 (b ∩ a) ≤ (c ∪ a)

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

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-le1 130  df-le2 131

This theorem is referenced by:  k1-4  359  u3lem15  795  bi4  840  negantlem9  859  negantlem10  861  mh  879  marsdenlem4  883  cancellem  891  e2ast2  894  lem4.6.6i0j4  1091  lem4.6.6i2j4  1097  lem4.6.6i3j1  1099  lem4.6.6i4j0  1100  lem4.6.6i4j2  1101  dp53lemf  1168  xdp53  1200  xxdp53  1203  xdp43lem  1205  xdp43  1207  3dp43  1208