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

Theorem or1 104
Description: Disjunction with 1.
Assertion
Ref Expression
or1 (a v 1) = 1

Proof of Theorem or1
StepHypRef Expression
1 df-t 41 . . . 4 1 = (a v a')
21lor 70 . . 3 (a v 1) = (a v (a v a'))
3 ax-a4 33 . . 3 (a v (a v a')) = (a v a')
42, 3ax-r2 36 . 2 (a v 1) = (a v a')
51ax-r1 35 . 2 (a v a') = 1
64, 5ax-r2 36 1 (a v 1) = 1
Colors of variables: term
Syntax hints:   = wb 1  'wn 4   v wo 6  1wt 8
This theorem is referenced by:  or1r  105  an0  108  le1  146  sklem  230  0i1  273  wle1  389  ska2  432  woml6  436  oml6  488  i3con  551  ud1lem3  562  ud3lem1c  568  ud3lem3  576  ud4lem1c  579  ud4lem1  581  ud4lem3b  584  ud5lem1  589  u1lemoa  620  u4lemoa  623  u2lemonb  636  u3lemonb  637  u4lem5  764  u4lem6  768  u1lem11  780  u3lem8  783  u3lem11  786  test  802  2oalem1  825  oa6v4v  933  lem3.3.7i0e1  1057  lem3.3.7i3e2  1067
This theorem was proved from axioms:  ax-a2 31  ax-a4 33  ax-r1 35  ax-r2 36  ax-r5 38
This theorem depends on definitions:  df-t 41
  Copyright terms: Public domain W3C validator