Theorem lear 153

Description: L.e. absorption.

Assertion

Ref	Expression
lear	(a ∩ b) ≤ b

Proof of Theorem lear

Step	Hyp	Ref	Expression
1		ancom 68	. 2 (a ∩ b) = (b ∩ a)
2		lea 152	. 2 (b ∩ a) ≤ b
3	1, 2	bltr 130	1 (a ∩ b) ≤ b

Syntax hints:   ≤ wle 2   ∩ wa 7

This theorem is referenced by:  leao2 155  leao4 157  womao 212  womaon 213  womaa 214  womaan 215  anorabs2 216  anorabs 217  ska15 236  mccune2 239  wql1lem 279  oaidlem1 286  womle 290  nom14 303  nom15 304  go1 335  i2or 336  i5lei2 340  wr5-2v 348  ska4 415  i3th5 529  ud3lem1c 550  ud3lem1d 551  ud3lem3a 554  ud3lem3d 557  ud3lem3 558  ud4lem1b 560  ud4lem1c 561  ud5lem1b 569  ud5lem1 571  u4lemab 595  u5lemab 596  u4lemona 610  u1lemob 612  u3lemob 614  u4lemob 615  u5lemob 616  u3lemonb 619  u4lemonb 620  u5lemonb 621  comi1 691  u12lembi 708  u4lem2 729  u4lem5 746  u4lem6 750  u24lem 752  u12lem 753  u3lem14mp 776  bi1o1a 780  biao 781  i2i1i1 782  3vth1 786  3vth2 787  3vded22 800  1oa 802  1oaii 806  2oalem1 807  oale 811  oaeqv 812  3vroa 813  mlalem 814  sa5 818  bi3 821  orbi 824  negantlem2 831  negantlem9 841  negantlem10 843  neg3antlem2 847  elimconslem 849  elimcons 850  comanblem1 852  mhlem 858  marsdenlem3 864  mlaconjo 868  oago3.29 871  cancellem 873  kb10iii 875  govar 876  gomaex3h4 885  gomaex3h8 889  oas 905  oatr 908  oaur 910  oaidlem2 911  oaidlem2g 912  distoa 924  oa3to4lem4 928  oa4b 939  oa4to4u2 954  oa3-u1 971  oa3-u2 972  oa3-1to5 973  d3oa 975  oalii 982  oacom2 992  oadistd 1003  4oaiii 1019  4oadist 1023

This theorem was proved from axioms:  ax-a2 30  ax-a5 33  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37

This theorem depends on definitions:  df-a 39  df-le1 122  df-le2 123

metamath.org