QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  wql2lem2 Unicode version
Theorem wql2lem2 289
Description: Lemma for ->2 WQL axiom.
Hypothesis
Ref Expression
wql2lem2.1 ((a v c) ->2 (b v c)) = 1
Assertion
Ref Expression
wql2lem2 ((a v (b v c))' v (b v c)) = 1
Proof of Theorem wql2lem2
StepHypRef Expression
1 df-i2 45 . . . 4 ((a v c) ->2 (b v c)) = ((b v c) v ((a v c)' ^ (b v c)'))
2 anor3 90 . . . . . 6 ((a v c)' ^ (b v c)') = ((a v c) v (b v c))'
3 ax-a3 32 . . . . . . . . . 10 ((a v b) v c) = (a v (b v c))
43ax-r1 35 . . . . . . . . 9 (a v (b v c)) = ((a v b) v c)
5 orordir 113 . . . . . . . . 9 ((a v b) v c) = ((a v c) v (b v c))
64, 5ax-r2 36 . . . . . . . 8 (a v (b v c)) = ((a v c) v (b v c))
76ax-r4 37 . . . . . . 7 (a v (b v c))' = ((a v c) v (b v c))'
87ax-r1 35 . . . . . 6 ((a v c) v (b v c))' = (a v (b v c))'
92, 8ax-r2 36 . . . . 5 ((a v c)' ^ (b v c)') = (a v (b v c))'
109lor 70 . . . 4 ((b v c) v ((a v c)' ^ (b v c)')) = ((b v c) v (a v (b v c))')
11 ax-a2 31 . . . 4 ((b v c) v (a v (b v c))') = ((a v (b v c))' v (b v c))
121, 10, 113tr 65 . . 3 ((a v c) ->2 (b v c)) = ((a v (b v c))' v (b v c))
1312ax-r1 35 . 2 ((a v (b v c))' v (b v c)) = ((a v c) ->2 (b v c))
14 wql2lem2.1 . 2 ((a v c) ->2 (b v c)) = 1
1513, 14ax-r2 36 1 ((a v (b v c))' v (b v c)) = 1
Colors of variables: term
Syntax hints:   = wb 1  'wn 4   v wo 6   ^ wa 7  1wt 8   ->2 wi2 13
This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38
This theorem depends on definitions:  df-a 40  df-t 41  df-f 42  df-i2 45
This theorem is referenced by:  wql2lem4  291
  Copyright terms: Public domain W3C validator