Theorem lea 152

Description: L.e. absorption.

Assertion

Ref	Expression
lea	(a ^ b) =< a

Proof of Theorem lea

Step	Hyp	Ref	Expression
1		ax-a2 30	. . 3 ((a ^ b) v a) = (a v (a ^ b))
2		a5b 112	. . 3 (a v (a ^ b)) = a
3	1, 2	ax-r2 35	. 2 ((a ^ b) v a) = a
4	3	df-le1 122	1 (a ^ b) =< a

Syntax hints:   =< wle 2   v wo 6   ^ wa 7

This theorem is referenced by:  lear 153  leao1 154  leao3 156  ledi 166  coman1 177  distlem 180  womao 212  womaon 213  womaa 214  womaan 215  anorabs2 216  anorabs 217  ska13 233  ska15 236  mccune2 239  wql2lem 280  nom13 302  nom14 303  nom20 305  nom21 306  nom22 307  i2or 336  i5lei1 339  2vwomlem 347  wr5-2v 348  wdf-c2 366  ska4 415  com3i 449  oml4 469  gsth 471  cmtr1com 475  i0cmtrcom 477  i3bi 478  i3or 479  df2i3 480  dfi3b 481  oi3ai3 485  lem4 493  bii3 498  i3th5 529  i3con 533  i3orlem7 540  ud3lem1a 548  ud3lem1c 550  ud3lem3a 554  ud3lem3d 557  ud3lem3 558  ud4lem1a 559  ud4lem1b 560  ud4lem1c 561  ud4lem1 563  ud4lem3a 565  ud4lem3b 566  ud5lem1b 569  ud5lem1 571  u3lemana 589  u3lemoa 604  u2lemona 608  u3lemona 609  u4lemona 610  u5lemona 611  u3lemob 614  u1lemc6 688  comi12 689  i2bi 704  u4lem1 719  u4lem6 750  u1lem8 758  u1lem9a 759  u3lem13a 771  u3lem13b 772  u3lemax4 778  u3lemax5 779  bi1o1a 780  test2 785  1oa 802  oaeqv 812  3vroa 813  mlalem 814  sa5 818  sadm3 820  bi3 821  imp3 823  orbi 824  mlaconj4 826  negantlem2 831  negantlem3 832  negantlem10 843  neg3antlem1 846  elimcons 850  elimcons2 851  comanblem1 852  comanb 854  mh 861  marsdenlem3 864  mlaconjo 868  distid 869  oago3.21x 872  cancellem 873  govar 876  gon2n 878  gomaex3h5 886  gomaex3h10 891  oas 905  oat 907  oau 909  oal42 915  oa23 916  oa3-u1lem 965  oa3-u2lem 966  d3oa 975  oaliv 983  oacom2 992  oagen1 994  mloa 998  oadistc0 1001  oadistc 1002  oadistd 1003  oa43v 1008  oa63v 1011  4oagen1 1021  4oadist 1023

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

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

metamath.org