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

Theorem le2or 168
Description: Disjunction of 2 l.e.'s. (Contributed by NM, 25-Oct-1997.)
Hypotheses
Ref Expression
le2.1 ab
le2.2 cd
Assertion
Ref Expression
le2or (ac) ≤ (bd)

Proof of Theorem le2or
StepHypRef Expression
1 le2.1 . . 3 ab
21leror 152 . 2 (ac) ≤ (bc)
3 le2.2 . . 3 cd
43lelor 166 . 2 (bc) ≤ (bd)
52, 4letr 137 1 (ac) ≤ (bd)
Colors of variables: term
Syntax hints:  wle 2  wo 6
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-t 41  df-f 42  df-le1 130  df-le2 131
This theorem is referenced by:  lel2or  170  ler2or  172  ledi  174  ledio  176  ska15  244  id5leid0  351  ska2  432  ka4ot  435  i3bi  496  lem4  511  binr3  519  i3th5  547  3vcom  813  3vded22  818  sadm3  838  mlaconjo  886  govar  896  distoa  944  oa3to4lem3  947  oa4to6lem4  963  oa4uto4g  975  oa4uto4  977  oa3-u2lem  986  d3oa  995  oadistd  1023  4oadist  1044  dp15lemf  1159  dp35lemd  1174  dp41lemh  1190  dp41leml  1193  xdp41  1198  xdp15  1199  xxdp41  1201  xxdp15  1202  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208
  Copyright terms: Public domain W3C validator