Theorem leao1 162

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

Assertion

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

Proof of Theorem leao1

Step	Hyp	Ref	Expression
1		lea 160	. 2 (a ∩ b) ≤ a
2		leo 158	. 2 a ≤ (a ∪ c)
3	1, 2	letr 137	1 (a ∩ b) ≤ (a ∪ c)

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:  biao  799  mlaconj4  844  negantlem9  859  neg3antlem2  865  elimconslem  867  mhlem  876  mh  879  mlaconjolem  885  mlaconjo  886  lem4.6.2e1  1080  lem4.6.6i0j2  1087  lem4.6.6i0j3  1088  lem4.6.6i0j4  1089  lem4.6.6i2j0  1093  lem4.6.6i2j1  1094  lem4.6.6i2j4  1095  lem4.6.6i3j0  1096  lem4.6.6i3j1  1097  lem4.6.6i4j0  1098  lem4.6.6i4j2  1099  ml3le  1127  vneulem7  1135  vneulem12  1140  vneulem13  1141  vneulemexp  1146  dp15lemf  1157  dp41leme  1185  dp41lemf  1186  dp32  1194  xdp41  1196  xdp15  1197  xxdp41  1199  xxdp15  1200  xdp45lem  1202  xdp43lem  1203  xdp45  1204  xdp43  1205  3dp43  1206  testmod  1211  testmod2  1213  testmod2expanded  1214