QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  wfh3 Unicode version
Theorem wfh3 425
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
wfh3 ((a v (b ^ c)) == ((a v b) ^ (a v c))) = 1
Proof of Theorem wfh3
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, 4wfh1 423 . . 3 ((a' ^ (b' v c')) == ((a' ^ b') v (a' ^ c'))) = 1
6 anor2 89 . . . . 5 (a' ^ (b' v c')) = (a v (b' v c')')'
76bi1 118 . . . 4 ((a' ^ (b' v c')) == (a v (b' v c')')') = 1
8 df-a 40 . . . . . . . 8 (b ^ c) = (b' v c')'
98bi1 118 . . . . . . 7 ((b ^ c) == (b' v c')') = 1
109wr1 197 . . . . . 6 ((b' v c')' == (b ^ c)) = 1
1110wlor 368 . . . . 5 ((a v (b' v c')') == (a v (b ^ c))) = 1
1211wr4 199 . . . 4 ((a v (b' v c')')' == (a v (b ^ c))') = 1
137, 12wr2 371 . . 3 ((a' ^ (b' v c')) == (a v (b ^ c))') = 1
14 oran 87 . . . . 5 ((a' ^ b') v (a' ^ c')) = ((a' ^ b')' ^ (a' ^ c')')'
1514bi1 118 . . . 4 (((a' ^ b') v (a' ^ c')) == ((a' ^ b')' ^ (a' ^ c')')') = 1
16 oran 87 . . . . . . . 8 (a v b) = (a' ^ b')'
1716bi1 118 . . . . . . 7 ((a v b) == (a' ^ b')') = 1
18 oran 87 . . . . . . . 8 (a v c) = (a' ^ c')'
1918bi1 118 . . . . . . 7 ((a v c) == (a' ^ c')') = 1
2017, 19w2an 373 . . . . . 6 (((a v b) ^ (a v c)) == ((a' ^ b')' ^ (a' ^ c')')) = 1
2120wr1 197 . . . . 5 (((a' ^ b')' ^ (a' ^ c')') == ((a v b) ^ (a v c))) = 1
2221wr4 199 . . . 4 (((a' ^ b')' ^ (a' ^ c')')' == ((a v b) ^ (a v c))') = 1
2315, 22wr2 371 . . 3 (((a' ^ b') v (a' ^ c')) == ((a v b) ^ (a v c))') = 1
245, 13, 23w3tr2 375 . 2 ((a v (b ^ c))' == ((a v b) ^ (a v c))') = 1
2524wcon1 207 1 ((a v (b ^ c)) == ((a v b) ^ (a 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:  woml7  437  wddi3  1107
  Copyright terms: Public domain W3C validator