Quantum Logic Explorer		< Previous   Next > Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  leao3		Unicode version

---

Theorem leao3 164

Description: L.e. absorption.

Assertion

Ref	Expression
leao3

---

Proof of Theorem leao3

Step	Hyp	Ref	Expression
1		lea 160	. 2
2		leor 159	. 2
3	1, 2	letr 137	1

Colors of variables: term

Syntax hints:   wle 2   wo 6   wa 7

This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  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:  mhlem2  878  mh  879  marsdenlem4  883  mhcor1  888  vneulem6  1134  vneulemexp  1146  dp41lemh  1188  dp41lemk  1190  xdp41  1196  xxdp41  1199  xdp45lem  1202  xdp43lem  1203  xdp45  1204  xdp43  1205  3dp43  1206

Copyright terms: Public domain

W3C validator