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.
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  1092  lem4.6.6i2j1  1094  lem4.6.7  1101  vneulem6  1134  vneulemexp  1146  dp41lemc0  1182  xdp41  1196  xxdp41  1199  xdp45lem  1202  xdp43lem  1203  xdp45  1204  xdp43  1205  3dp43  1206  testmod2  1213  testmod2expanded  1214  testmod3  1215
 Copyright terms: Public domain W3C validator