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

Theorem ler 149
 Description: Add disjunct to right of l.e. (Contributed by NM, 27-Aug-1997.)
Hypothesis
Ref Expression
le.1 ab
Assertion
Ref Expression
ler a ≤ (bc)

Proof of Theorem ler
StepHypRef Expression
1 ax-a3 32 . . . 4 ((ab) ∪ c) = (a ∪ (bc))
21ax-r1 35 . . 3 (a ∪ (bc)) = ((ab) ∪ c)
3 le.1 . . . . 5 ab
43df-le2 131 . . . 4 (ab) = b
54ax-r5 38 . . 3 ((ab) ∪ c) = (bc)
62, 5ax-r2 36 . 2 (a ∪ (bc)) = (bc)
76df-le1 130 1 a ≤ (bc)
 Colors of variables: term Syntax hints:   ≤ wle 2   ∪ wo 6 This theorem was proved from axioms:  ax-a3 32  ax-r1 35  ax-r2 36  ax-r5 38 This theorem depends on definitions:  df-le1 130  df-le2 131 This theorem is referenced by:  lerr  150  i3orlem4  555  i3orlem7  558  i3orlem8  559  negantlem9  859  negantlem10  861  neg3antlem2  865  mhlemlem1  874  e2astlem1  895  lem3.4.3  1076  lem4.6.6i1j3  1094  lem4.6.6i2j1  1096  lem4.6.7  1103  vneulem6  1136  vneulemexp  1148  dp41lemc0  1184  xdp41  1198  xxdp41  1201  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208  testmod2  1215  testmod2expanded  1216  testmod3  1217
 Copyright terms: Public domain W3C validator