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

Theorem or0r 103
Description: Disjunction with 0. (Contributed by NM, 26-Nov-1997.)
Assertion
Ref Expression
or0r (0 ∪ a) = a

Proof of Theorem or0r
StepHypRef Expression
1 ax-a2 31 . 2 (0 ∪ a) = (a ∪ 0)
2 or0 102 . 2 (a ∪ 0) = a
31, 2ax-r2 36 1 (0 ∪ a) = a
Colors of variables: term
Syntax hints:   = wb 1  wo 6  0wf 9
This theorem was proved from axioms:  ax-a2 31  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38
This theorem depends on definitions:  df-t 41  df-f 42
This theorem is referenced by:  k1-4  359  ud3lem1a  566  ud3lem1d  569  ud5lem1b  587  bi1o1a  798  bi3  839  bi4  840  mlaconj4  844  mhlemlem1  874  mhlem1  877  marsdenlem2  881  mlaconjo  886  mhcor1  888  e2astlem1  895  oa6v4v  933  lem3.3.4  1053  lem3.3.7i3e1  1066  vneulem3  1133  vneulem7  1137  vneulem13  1143  vneulemexp  1148
  Copyright terms: Public domain W3C validator