Theorem lea 160

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

Assertion

Ref	Expression
lea	(a ∩ b) ≤ a

Proof of Theorem lea

Step	Hyp	Ref	Expression
1		ax-a2 31	. . 3 ((a ∩ b) ∪ a) = (a ∪ (a ∩ b))
2		orabs 120	. . 3 (a ∪ (a ∩ b)) = a
3	1, 2	ax-r2 36	. 2 ((a ∩ b) ∪ a) = a
4	3	df-le1 130	1 (a ∩ b) ≤ a

Syntax hints:   ≤ wle 2   ∪ wo 6   ∩ wa 7

This theorem was proved from axioms:  ax-a2 31  ax-a5 34  ax-r1 35  ax-r2 36  ax-r5 38

This theorem depends on definitions:  df-a 40  df-le1 130

This theorem is referenced by:  lear  161  leao1  162  leao3  164  ledi  174  coman1  185  distlem  188  womao  220  womaon  221  womaa  222  womaan  223  anorabs2  224  ska13  241  ska15  244  mccune2  247  wql2lem  288  nom13  310  nom14  311  nom20  313  nom21  314  nom22  315  i2or  344  i5lei1  347  id5leid0  351  2vwomlem  365  wr5-2v  366  wdf-c2  384  ska4  433  com3i  467  oml4  487  gsth  489  cmtr1com  493  i0cmtrcom  495  i3bi  496  i3or  497  df2i3  498  dfi3b  499  oi3ai3  503  lem4  511  bii3  516  i3th5  547  i3con  551  i3orlem7  558  ud3lem1a  566  ud3lem1c  568  ud3lem3a  572  ud3lem3d  575  ud3lem3  576  ud4lem1a  577  ud4lem1b  578  ud4lem1c  579  ud4lem1  581  ud4lem3a  583  ud4lem3b  584  ud5lem1b  587  ud5lem1  589  u3lemana  607  u3lemoa  622  u2lemona  626  u3lemona  627  u4lemona  628  u5lemona  629  u3lemob  632  u1lemc6  706  comi12  707  i2bi  722  u4lem1  737  u4lem6  768  u1lem8  776  u1lem9a  777  u3lem13a  789  u3lem13b  790  u3lemax4  796  u3lemax5  797  bi1o1a  798  test2  803  1oa  820  oaeqv  830  3vroa  831  mlalem  832  sa5  836  sadm3  838  bi3  839  imp3  841  orbi  842  mlaconj4  844  negantlem2  849  negantlem3  850  negantlem10  861  neg3antlem1  864  elimcons  868  elimcons2  869  comanblem1  870  comanb  872  mh  879  marsdenlem3  882  mlaconjo  886  distid  887  oago3.21x  890  cancellem  891  govar  896  gon2n  898  gomaex3h5  906  gomaex3h10  911  oas  925  oat  927  oau  929  oal42  935  oa23  936  oa3-u1lem  985  oa3-u2lem  986  d3oa  995  oaliv  1003  oacom2  1012  oagen1  1014  mloa  1018  oadistc0  1021  oadistc  1022  oadistd  1023  oa43v  1028  oa63v  1032  4oagen1  1042  4oadist  1044  lem3.3.3lem1  1049  lem3.3.5  1055  lem3.3.7i2e2  1064  lem3.3.7i3e2  1067  lem3.3.7i4e1  1069  lem3.3.7i4e2  1070  lem3.3.7i5e1  1072  lem3.4.3  1076  lem4.6.6i0j4  1091  lem4.6.6i1j3  1094  lem4.6.6i4j0  1100  l42modlem2  1150  dp15lema  1154  dp15lemf  1159  dp53lema  1163  dp53lemd  1166  dp53leme  1167  dp53lemf  1168  dp35lemd  1174  dp35lem0  1179  dp41lemd  1186  dp41lemh  1190  dp32  1196  dp23  1197  xdp41  1198  xdp15  1199  xdp53  1200  xxdp41  1201  xxdp15  1202  xxdp53  1203  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208  testmod2  1215  testmod2expanded  1216