QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  lear Unicode version
Theorem lear 161
Description: L.e. absorption.
Assertion
Ref Expression
lear (a ^ b) =< b
Proof of Theorem lear
StepHypRef Expression
1 ancom 74 . 2 (a ^ b) = (b ^ a)
2 lea 160 . 2 (b ^ a) =< b
31, 2bltr 138 1 (a ^ b) =< b
Colors of variables: term
Syntax hints:   =< wle 2   ^ wa 7
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
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  1040  4oadist  1044  lem3.3.3lem2  1050  lem3.3.7i4e1  1069  lem3.3.7i4e2  1070  lem3.3.7i5e1  1072  lem4.6.2e1  1080  lem4.6.6i0j1  1086  lem4.6.6i0j3  1088  lem4.6.6i1j0  1090  lem4.6.6i1j3  1092  lem4.6.6i2j1  1094  com3iia  1100  mldual2i  1125  ml3le  1127  vneulem1  1129  vneulem13  1141  vneulemexp  1146  dp15lema  1152  dp53lema  1161  dp53leme  1165  dp35lemd  1172  dp35lema  1176  dp35lem0  1177  dp34  1179  dp41leme  1185  dp41lemh  1188  xdp41  1196  xdp15  1197  xdp53  1198  xxdp41  1199  xxdp15  1200  xxdp53  1201  xdp45lem  1202  xdp43lem  1203  xdp45  1204  xdp43  1205  3dp43  1206
  Copyright terms: Public domain W3C validator