Theorem lea 160

Description: L.e. absorption.

Assertion

Ref	Expression
lea	(a ^ b) =< a

Proof of Theorem lea

Step	Hyp	Ref	Expression
1		ax-a2 31	. . 3 ((a ^ b) v a) = (a v (a ^ b))
2		a5b 120	. . 3 (a v (a ^ b)) = a
3	1, 2	ax-r2 36	. 2 ((a ^ b) v a) = a
4	3	df-le1 130	1 (a ^ b) =< a

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

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 1031  4oagen1 1041  4oadist 1043  lem3.3.3lem1 1048  lem3.3.5 1054  lem3.3.7i2e2 1063  lem3.3.7i3e2 1066  lem3.3.7i4e1 1068  lem3.3.7i4e2 1069  lem3.3.7i5e1 1071  lem3.4.3 1075  lem4.6.6i0j4 1088  lem4.6.6i1j3 1091  lem4.6.6i4j0 1097

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

Copyright terms: Public domain