Theorem leao4 165

Description: L.e. absorption.

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  1089  lem4.6.6i2j4  1095  lem4.6.6i3j1  1097  lem4.6.6i4j0  1098  lem4.6.6i4j2  1099  dp53lemf  1166  xdp53  1198  xxdp53  1201  xdp43lem  1203  xdp43  1205  3dp43  1206