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

Theorem orabs 120
 Description: Absorption law.
Assertion
Ref Expression
orabs (a ∪ (ab)) = a

Proof of Theorem orabs
StepHypRef Expression
1 df-a 40 . . 3 (ab) = (ab )
21lor 70 . 2 (a ∪ (ab)) = (a ∪ (ab ) )
3 ax-a5 34 . 2 (a ∪ (ab ) ) = a
42, 3ax-r2 36 1 (a ∪ (ab)) = a
 Colors of variables: term Syntax hints:   = wb 1  ⊥ wn 4   ∪ wo 6   ∩ wa 7 This theorem was proved from axioms:  ax-a2 31  ax-a5 34  ax-r1 35  ax-r2 36  ax-r5 38 This theorem depends on definitions:  df-a 40 This theorem is referenced by:  leao  124  omlem1  127  lea  160  lecom  180  wa5b  200  nom12  309  nom13  310  wcomlem  382  wlecom  409  oml5  449  comcom  453  i3lem3  506  lem4  511  i3abs1  522  i3th1  543  i3con  551  ud1lem1  560  ud2lem3  565  ud3lem1  570  ud3lem3c  574  ud5lem3  594  u5lemaa  604  u5lemoa  624  u12lem  771  u3lem7  774  u1lem11  780  u3lem10  785  i1abs  801  test  802  3vded3  819  1oaii  824  sa5  836  neg3antlem2  865  gomaex3lem3  916  oau  929  oa23  936  oa3-6lem  980  oalii  1002  oalem2  1006  lem3.3.7i2e2  1064  lem3.3.7i3e1  1066  lem3.3.7i3e2  1067  lem4.6.2e1  1080  dp15lemd  1155  xdp15  1197  xxdp15  1200  xdp45lem  1202  xdp43lem  1203  xdp45  1204  xdp43  1205  3dp43  1206
 Copyright terms: Public domain W3C validator