Theorem lear 161

Description: L.e. absorption.

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 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 1039  4oadist 1043  lem3.3.3lem2 1049  lem3.3.7i4e1 1068  lem3.3.7i4e2 1069  lem3.3.7i5e1 1071  lem4.6.2e1 1079  lem4.6.6i0j1 1085  lem4.6.6i0j3 1087  lem4.6.6i1j0 1089  lem4.6.6i1j3 1091  lem4.6.6i2j1 1093  com3iia 1099

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

Copyright terms: Public domain