QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  wlem14 Unicode version
Theorem wlem14 430
Description: Lemma for KA14 soundness.
Assertion
Ref Expression
wlem14 (((a ^ b') v a')' v ((a ^ b') v ((a' ^ ((a v b') ^ (a v b))) v (a' ^ ((a v b') ^ (a v b))')))) = 1
Proof of Theorem wlem14
StepHypRef Expression
1 df-t 41 . . . 4 1 = (((a ^ b') v a') v ((a ^ b') v a')')
21ax-r1 35 . . 3 (((a ^ b') v a') v ((a ^ b') v a')') = 1
3 ax-a2 31 . . . 4 (((a ^ b') v a')' v ((a ^ b') v a')) = (((a ^ b') v a') v ((a ^ b') v a')')
43bi1 118 . . 3 ((((a ^ b') v a')' v ((a ^ b') v a')) == (((a ^ b') v a') v ((a ^ b') v a')')) = 1
52, 4wwbmpr 206 . 2 (((a ^ b') v a')' v ((a ^ b') v a')) = 1
6 df-t 41 . . . . . . . 8 1 = (((a v b') ^ (a v b)) v ((a v b') ^ (a v b))')
76ax-r1 35 . . . . . . 7 (((a v b') ^ (a v b)) v ((a v b') ^ (a v b))') = 1
87bi1 118 . . . . . 6 ((((a v b') ^ (a v b)) v ((a v b') ^ (a v b))') == 1) = 1
98wlan 370 . . . . 5 ((a' ^ (((a v b') ^ (a v b)) v ((a v b') ^ (a v b))')) == (a' ^ 1)) = 1
10 anidm 111 . . . . . . . . . . 11 (a ^ a) = a
1110bi1 118 . . . . . . . . . 10 ((a ^ a) == a) = 1
1211wr1 197 . . . . . . . . 9 (a == (a ^ a)) = 1
13 wleo 387 . . . . . . . . . 10 (a =<2 (a v b')) = 1
14 wleo 387 . . . . . . . . . 10 (a =<2 (a v b)) = 1
1513, 14wle2an 404 . . . . . . . . 9 ((a ^ a) =<2 ((a v b') ^ (a v b))) = 1
1612, 15wbltr 397 . . . . . . . 8 (a =<2 ((a v b') ^ (a v b))) = 1
1716wlecom 409 . . . . . . 7 C (a, ((a v b') ^ (a v b))) = 1
1817wcomcom3 416 . . . . . 6 C (a', ((a v b') ^ (a v b))) = 1
1917wcomcom4 417 . . . . . 6 C (a', ((a v b') ^ (a v b))') = 1
2018, 19wfh1 423 . . . . 5 ((a' ^ (((a v b') ^ (a v b)) v ((a v b') ^ (a v b))')) == ((a' ^ ((a v b') ^ (a v b))) v (a' ^ ((a v b') ^ (a v b))'))) = 1
21 an1 106 . . . . . 6 (a' ^ 1) = a'
2221bi1 118 . . . . 5 ((a' ^ 1) == a') = 1
239, 20, 22w3tr2 375 . . . 4 (((a' ^ ((a v b') ^ (a v b))) v (a' ^ ((a v b') ^ (a v b))')) == a') = 1
2423wlor 368 . . 3 (((a ^ b') v ((a' ^ ((a v b') ^ (a v b))) v (a' ^ ((a v b') ^ (a v b))'))) == ((a ^ b') v a')) = 1
2524wlor 368 . 2 ((((a ^ b') v a')' v ((a ^ b') v ((a' ^ ((a v b') ^ (a v b))) v (a' ^ ((a v b') ^ (a v b))')))) == (((a ^ b') v a')' v ((a ^ b') v a'))) = 1
265, 25wwbmpr 206 1 (((a ^ b') v a')' v ((a ^ b') v ((a' ^ ((a v b') ^ (a v b))) v (a' ^ ((a v b') ^ (a v b))')))) = 1
Colors of variables: term
Syntax hints:   = wb 1  'wn 4   v wo 6   ^ wa 7  1wt 8
This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a4 33  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-wom 361
This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i1 44  df-i2 45  df-le 129  df-le1 130  df-le2 131  df-cmtr 134
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator