Theorem lear 161

Description: L.e. absorption. (Contributed by NM, 11-Nov-1997.)

Assertion

Ref	Expression
lear	(a ∩ b) ≤ b

Proof of Theorem lear

Step	Hyp	Ref	Expression
1		ancom 74	. 2 (a ∩ b) = (b ∩ a)
2		lea 160	. 2 (b ∩ a) ≤ b
3	1, 2	bltr 138	1 (a ∩ b) ≤ b

Syntax hints:   ≤ wle 2   ∩ wa 7

This theorem was proved from axioms:  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  df-le2 131

This theorem is referenced by:  leao2  163  leao4  165  womao  220  womaon  221  womaa  222  womaan  223  anorabs2  224  ska15  244  mccune2  247  wql1lem  287  oaidlem1  294  womle  298  nom14  311  nom15  312  go1  343  i2or  344  i5lei2  348  id5leid0  351  k1-2  357  k1-3  358  wr5-2v  366  ska4  433  i3th5  547  ud3lem1c  568  ud3lem1d  569  ud3lem3a  572  ud3lem3d  575  ud3lem3  576  ud4lem1b  578  ud4lem1c  579  ud5lem1b  587  ud5lem1  589  u4lemab  613  u5lemab  614  u4lemona  628  u1lemob  630  u3lemob  632  u4lemob  633  u5lemob  634  u3lemonb  637  u4lemonb  638  u5lemonb  639  comi1  709  u12lembi  726  u4lem2  747  u4lem5  764  u4lem6  768  u24lem  770  u12lem  771  u3lem14mp  794  bi1o1a  798  biao  799  i2i1i1  800  3vth1  804  3vth2  805  3vded22  818  1oa  820  1oaii  824  2oalem1  825  oale  829  oaeqv  830  3vroa  831  mlalem  832  sa5  836  bi3  839  orbi  842  negantlem2  849  negantlem9  859  negantlem10  861  neg3antlem2  865  elimconslem  867  elimcons  868  comanblem1  870  mhlem  876  marsdenlem3  882  mlaconjo  886  oago3.29  889  cancellem  891  kb10iii  893  e2ast2  894  govar  896  gomaex3h4  905  gomaex3h8  909  oas  925  oatr  928  oaur  930  oaidlem2  931  oaidlem2g  932  distoa  944  oa3to4lem4  948  oa4b  959  oa4to4u2  974  oa3-u1  991  oa3-u2  992  oa3-1to5  993  d3oa  995  oalii  1002  oacom2  1012  oadistd  1023  4oaiii  1040  4oadist  1044  lem3.3.3lem2  1050  lem3.3.7i4e1  1069  lem3.3.7i4e2  1070  lem3.3.7i5e1  1072  lem4.6.2e1  1082  lem4.6.6i0j1  1088  lem4.6.6i0j3  1090  lem4.6.6i1j0  1092  lem4.6.6i1j3  1094  lem4.6.6i2j1  1096  com3iia  1102  mldual2i  1127  ml3le  1129  vneulem1  1131  vneulem13  1143  vneulemexp  1148  dp15lema  1154  dp53lema  1163  dp53leme  1167  dp35lemd  1174  dp35lema  1178  dp35lem0  1179  dp34  1181  dp41leme  1187  dp41lemh  1190  xdp41  1198  xdp15  1199  xdp53  1200  xxdp41  1201  xxdp15  1202  xxdp53  1203  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208