Theorem leo 158

Description: L.e. absorption. (Contributed by NM, 27-Aug-1997.)

Assertion

Ref	Expression
leo	a ≤ (a ∪ b)

Proof of Theorem leo

Step	Hyp	Ref	Expression
1		anabs 121	. 2 (a ∩ (a ∪ b)) = a
2	1	df2le1 135	1 a ≤ (a ∪ b)

Syntax hints:   ≤ wle 2   ∪ wo 6

This theorem was proved from axioms:  ax-a1 30  ax-a2 31  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

This theorem is referenced by:  leor  159  leao1  162  leao2  163  ledio  176  comorr  184  distlem  188  womao  220  womaon  221  womaa  222  womaan  223  anorabs2  224  ka4lemo  228  bina3  284  bina4  285  nom14  311  nom21  314  nom22  315  nom24  317  i1or  345  i5lei4  350  k1-8a  355  2vwomlem  365  wr5-2v  366  ska2  432  gsth  489  i3bi  496  df2i3  498  dfi3b  499  oi3ai3  503  i3th8  550  i3con  551  i3orlem2  553  i3orlem4  555  i3orlem5  556  i3orlem7  558  ud3lem1a  566  ud3lem3d  575  ud3lem3  576  ud4lem1a  577  ud4lem1b  578  ud4lem1c  579  ud5lem1b  587  ud5lem1  589  u4lemana  608  u4lemona  628  u3lemob  632  u1lemc6  706  comi12  707  i2bi  722  u12lembi  726  u4lem1  737  u4lem6  768  u12lem  771  u1lem8  776  u1lem9b  778  u3lem13b  790  bi1o1a  798  test2  803  3vth6  809  3vded11  814  3vded12  815  2oalem1  825  mlalem  832  sadm3  838  bi3  839  orbi  842  negantlem1  848  negantlem2  849  negantlem3  850  negantlem9  859  neg3antlem1  864  neg3antlem2  865  comanb  872  mhlemlem1  874  mhlem  876  mh  879  cancellem  891  e2astlem1  895  gomaex3h3  904  gomaex3lem10  923  oas  925  oatr  928  oau  929  oa23  936  oa4lem1  937  distoah2  941  distoah4  943  oa3to4lem1  945  oa6to4h1  955  oa6to4h2  956  oa6to4h3  957  oa4to6lem1  960  oa4btoc  966  oa3-6lem  980  oa3-u1lem  985  oa3-2to2s  990  d3oa  995  d4oa  996  oaliv  1003  oadist2a  1007  mloa  1018  oadistd  1023  axoa4a  1037  4oadist  1044  lem3.3.5  1055  lem3.3.7i4e1  1069  lem4.6.6i0j1  1088  lem4.6.6i0j2  1089  lem4.6.6i0j3  1090  lem4.6.6i0j4  1091  lem4.6.6i1j3  1094  lem4.6.6i2j1  1096  lem4.6.6i3j0  1098  lem4.6.6i3j1  1099  lem4.6.6i4j2  1101  ml  1123  vneulem6  1136  vneulemexp  1148  l42modlem1  1149  dp53lema  1163  dp53lemc  1165  dp53lemf  1168  dp35lemf  1172  dp35leme  1173  dp35lemc  1175  dp35lema  1178  dp41lemb  1183  dp41lemc0  1184  dp41lemc  1185  dp41lemh  1190  xdp41  1198  xdp53  1200  xxdp41  1201  xxdp53  1203  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208  oadp35lemf  1210  oadp35lemc  1211  testmod  1213  testmod2  1215  testmod2expanded  1216