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  1082  lem4.6.6i0j2  1089  lem4.6.6i0j3  1090  lem4.6.6i0j4  1091  lem4.6.6i2j0  1095  lem4.6.6i2j1  1096  lem4.6.6i2j4  1097  lem4.6.6i3j0  1098  lem4.6.6i3j1  1099  lem4.6.6i4j0  1100  lem4.6.6i4j2  1101  ml3le  1129  vneulem7  1137  vneulem12  1142  vneulem13  1143  vneulemexp  1148  dp15lemf  1159  dp41leme  1187  dp41lemf  1188  dp32  1196  xdp41  1198  xdp15  1199  xxdp41  1201  xxdp15  1202  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208  testmod  1213  testmod2  1215  testmod2expanded  1216