QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  df-le2 Unicode version
Definition df-le2 131
Description: Define 'less than or equal to'. See df-le1 130 for the other direction.
Hypothesis
Ref Expression
df-le2.1 a =< b
Assertion
Ref Expression
df-le2 (a v b) = b
Detailed syntax breakdown of Definition df-le2
StepHypRef Expression
1 wva . . 3 term a
2 wvb . . 3 term b
31, 2wo 6 . 2 term (a v b)
43, 2wb 1 1 wff (a v b) = b
Colors of variables: term
This definition is referenced by:  df2le2  136  letr  137  bltr  138  lebi  145  ler  149  leror  152  lecon  154  wwoml2  212  sklem  230  nom13  310  nom14  311  nom15  312  k1-4  359  oml2  451  gsth  489  cmtr1com  493  i0cmtrcom  495  df2i3  498  oi3ai3  503  i3con  551  i3orlem6  557  ud3lem1c  568  ud3lem3  576  ud4lem1c  579  ud4lem1  581  ud4lem3b  584  ud5lem1  589  u3lemoa  622  u2lemona  626  u3lemona  627  u4lemona  628  u5lemona  629  u1lemob  630  u3lemob  632  u4lemob  633  u5lemob  634  u3lemonb  637  u4lemonb  638  u5lemonb  639  u4lem1  737  u4lem2  747  u4lem5  764  u4lem6  768  u24lem  770  u3lem13a  789  u3lem13b  790  biao  799  test  802  test2  803  3vth3  806  3vth6  809  orbi  842  elimconslem  867  elimcons  868  elimcons2  869  comanblem1  870  mhlem  876  e2ast2  894  gomaex3lem1  914  oaidlem2  931  oaidlem2g  932  oa3-6lem  980  oa3-u1lem  985  oa3-u2lem  986  oa3-u1  991  oa3-u2  992  oadistc0  1021  lem3.3.7i2e2  1064  lem3.3.7i3e2  1067  lem4.6.2e1  1080  lem4.6.6i1j0  1090  lem4.6.6i1j3  1092  lem4.6.6i2j0  1093  lem4.6.6i3j0  1096  lem4.6.6i4j0  1098  lem4.6.7  1101  ml2i  1123  vneulem12  1140  vneulemexp  1146  dp53lemc  1163  dp53lemf  1166  dp35lemc  1173  dp41leml  1191  dp32  1194  xdp41  1196  xdp53  1198  xxdp41  1199  xxdp53  1201  xdp45lem  1202  xdp43lem  1203  xdp45  1204  xdp43  1205  3dp43  1206  oadp35lemc  1209
  Copyright terms: Public domain W3C validator