QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  wfh4 Unicode version
Theorem wfh4 426
Description: Weak structural analog of Foulis-Holland Theorem.
Hypotheses
Ref Expression
wfh.1 C (a, b) = 1
wfh.2 C (a, c) = 1
Assertion
Ref Expression
wfh4 ((b v (a ^ c)) == ((b v a) ^ (b v c))) = 1
Proof of Theorem wfh4
StepHypRef Expression
1 wfh.1 . . . . 5 C (a, b) = 1
21wcomcom4 417 . . . 4 C (a', b') = 1
3 wfh.2 . . . . 5 C (a, c) = 1
43wcomcom4 417 . . . 4 C (a', c') = 1
52, 4wfh2 424 . . 3 ((b' ^ (a' v c')) == ((b' ^ a') v (b' ^ c'))) = 1
6 anor2 89 . . . . 5 (b' ^ (a' v c')) = (b v (a' v c')')'
76bi1 118 . . . 4 ((b' ^ (a' v c')) == (b v (a' v c')')') = 1
8 df-a 40 . . . . . . . 8 (a ^ c) = (a' v c')'
98bi1 118 . . . . . . 7 ((a ^ c) == (a' v c')') = 1
109wr1 197 . . . . . 6 ((a' v c')' == (a ^ c)) = 1
1110wlor 368 . . . . 5 ((b v (a' v c')') == (b v (a ^ c))) = 1
1211wr4 199 . . . 4 ((b v (a' v c')')' == (b v (a ^ c))') = 1
137, 12wr2 371 . . 3 ((b' ^ (a' v c')) == (b v (a ^ c))') = 1
14 oran 87 . . . . 5 ((b' ^ a') v (b' ^ c')) = ((b' ^ a')' ^ (b' ^ c')')'
1514bi1 118 . . . 4 (((b' ^ a') v (b' ^ c')) == ((b' ^ a')' ^ (b' ^ c')')') = 1
16 oran 87 . . . . . . . 8 (b v a) = (b' ^ a')'
1716bi1 118 . . . . . . 7 ((b v a) == (b' ^ a')') = 1
18 oran 87 . . . . . . . 8 (b v c) = (b' ^ c')'
1918bi1 118 . . . . . . 7 ((b v c) == (b' ^ c')') = 1
2017, 19w2an 373 . . . . . 6 (((b v a) ^ (b v c)) == ((b' ^ a')' ^ (b' ^ c')')) = 1
2120wr1 197 . . . . 5 (((b' ^ a')' ^ (b' ^ c')') == ((b v a) ^ (b v c))) = 1
2221wr4 199 . . . 4 (((b' ^ a')' ^ (b' ^ c')')' == ((b v a) ^ (b v c))') = 1
2315, 22wr2 371 . . 3 (((b' ^ a') v (b' ^ c')) == ((b v a) ^ (b v c))') = 1
245, 13, 23w3tr2 375 . 2 ((b v (a ^ c))' == ((b v a) ^ (b v c))') = 1
2524wcon1 207 1 ((b v (a ^ c)) == ((b v a) ^ (b v c))) = 1
Colors of variables: term
Syntax hints:   = wb 1  'wn 4   == tb 5   v wo 6   ^ wa 7  1wt 8   C wcmtr 29
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:  ska2  432  ska4  433  woml6  436
  Copyright terms: Public domain W3C validator