QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  leo Unicode version
Theorem leo 158
Description: L.e. absorption.
Assertion
Ref Expression
leo a =< (a v b)
Proof of Theorem leo
StepHypRef Expression
1 anabs 121 . 2 (a ^ (a v b)) = a
21df2le1 135 1 a =< (a v b)
Colors of variables: term
Syntax hints:   =< wle 2   v wo 6
This theorem was proved from axioms:  ax-a1 30  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
This theorem is referenced by:  leor  159  leao1  162  leao2  163  ledio  176  comorr  184  distlem  188  womao  220  womaon  221  womaa  222  womaan  223  anorabs2  224  ka4lemo  228  bina3  284  bina4  285  nom14  311  nom21  314  nom22  315  nom24  317  i1or  345  i5lei4  350  k1-8a  355  2vwomlem  365  wr5-2v  366  ska2  432  gsth  489  i3bi  496  df2i3  498  dfi3b  499  oi3ai3  503  i3th8  550  i3con  551  i3orlem2  553  i3orlem4  555  i3orlem5  556  i3orlem7  558  ud3lem1a  566  ud3lem3d  575  ud3lem3  576  ud4lem1a  577  ud4lem1b  578  ud4lem1c  579  ud5lem1b  587  ud5lem1  589  u4lemana  608  u4lemona  628  u3lemob  632  u1lemc6  706  comi12  707  i2bi  722  u12lembi  726  u4lem1  737  u4lem6  768  u12lem  771  u1lem8  776  u1lem9b  778  u3lem13b  790  bi1o1a  798  test2  803  3vth6  809  3vded11  814  3vded12  815  2oalem1  825  mlalem  832  sadm3  838  bi3  839  orbi  842  negantlem1  848  negantlem2  849  negantlem3  850  negantlem9  859  neg3antlem1  864  neg3antlem2  865  comanb  872  mhlemlem1  874  mhlem  876  mh  879  cancellem  891  e2astlem1  895  gomaex3h3  904  gomaex3lem10  923  oas  925  oatr  928  oau  929  oa23  936  oa4lem1  937  distoah2  941  distoah4  943  oa3to4lem1  945  oa6to4h1  955  oa6to4h2  956  oa6to4h3  957  oa4to6lem1  960  oa4btoc  966  oa3-6lem  980  oa3-u1lem  985  oa3-2to2s  990  d3oa  995  d4oa  996  oaliv  1003  oadist2a  1007  mloa  1018  oadistd  1023  axoa4a  1037  4oadist  1044  lem3.3.5  1055  lem3.3.7i4e1  1069  lem4.6.6i0j1  1086  lem4.6.6i0j2  1087  lem4.6.6i0j3  1088  lem4.6.6i0j4  1089  lem4.6.6i1j3  1092  lem4.6.6i2j1  1094  lem4.6.6i3j0  1096  lem4.6.6i3j1  1097  lem4.6.6i4j2  1099  ml  1121  vneulem6  1134  vneulemexp  1146  l42modlem1  1147  dp53lema  1161  dp53lemc  1163  dp53lemf  1166  dp35lemf  1170  dp35leme  1171  dp35lemc  1173  dp35lema  1176  dp41lemb  1181  dp41lemc0  1182  dp41lemc  1183  dp41lemh  1188  xdp41  1196  xdp53  1198  xxdp41  1199  xxdp53  1201  xdp45lem  1202  xdp43lem  1203  xdp45  1204  xdp43  1205  3dp43  1206  oadp35lemf  1208  oadp35lemc  1209  testmod  1211  testmod2  1213  testmod2expanded  1214
  Copyright terms: Public domain W3C validator