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

Theorem fh4 472
Description: Foulis-Holland Theorem.
Hypotheses
Ref Expression
fh.1 a C b
fh.2 a C c
Assertion
Ref Expression
fh4 (b v (a ^ c)) = ((b v a) ^ (b v c))

Proof of Theorem fh4
StepHypRef Expression
1 fh.1 . . . . 5 a C b
21comcom4 455 . . . 4 a' C b'
3 fh.2 . . . . 5 a C c
43comcom4 455 . . . 4 a' C c'
52, 4fh2 470 . . 3 (b' ^ (a' v c')) = ((b' ^ a') v (b' ^ c'))
6 anor2 89 . . . 4 (b' ^ (a' v c')) = (b v (a' v c')')'
7 df-a 40 . . . . . . 7 (a ^ c) = (a' v c')'
87ax-r1 35 . . . . . 6 (a' v c')' = (a ^ c)
98lor 70 . . . . 5 (b v (a' v c')') = (b v (a ^ c))
109ax-r4 37 . . . 4 (b v (a' v c')')' = (b v (a ^ c))'
116, 10ax-r2 36 . . 3 (b' ^ (a' v c')) = (b v (a ^ c))'
12 oran 87 . . . 4 ((b' ^ a') v (b' ^ c')) = ((b' ^ a')' ^ (b' ^ c')')'
13 oran 87 . . . . . . 7 (b v a) = (b' ^ a')'
14 oran 87 . . . . . . 7 (b v c) = (b' ^ c')'
1513, 142an 79 . . . . . 6 ((b v a) ^ (b v c)) = ((b' ^ a')' ^ (b' ^ c')')
1615ax-r1 35 . . . . 5 ((b' ^ a')' ^ (b' ^ c')') = ((b v a) ^ (b v c))
1716ax-r4 37 . . . 4 ((b' ^ a')' ^ (b' ^ c')')' = ((b v a) ^ (b v c))'
1812, 17ax-r2 36 . . 3 ((b' ^ a') v (b' ^ c')) = ((b v a) ^ (b v c))'
195, 11, 183tr2 64 . 2 (b v (a ^ c))' = ((b v a) ^ (b v c))'
2019con1 66 1 (b v (a ^ c)) = ((b v a) ^ (b v c))
Colors of variables: term
Syntax hints:   = wb 1   C wc 3  'wn 4   v wo 6   ^ wa 7
This theorem is referenced by:  fh4r  476  fh4c  478  df2i3  498  i3abs3  524  i3con  551  ud3lem1c  568  ud4lem1c  579  ud4lem1  581  ud5lem1  589  ud5lem3  594  u5lemaa  604  u4lemona  628  u3lemob  632  u3lemonb  637  u1lemc4  701  u2lemc4  702  u3lemc4  703  u4lemc4  704  u5lemc4  705  u4lem1  737  u2lem3  750  u1lem4  757  u4lem5  764  u5lem5  765  u4lem6  768  u5lem6  769  u3lem11  786  orbi  842  e2ast2  894
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-r3 439
This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-le1 130  df-le2 131  df-c1 132  df-c2 133
  Copyright terms: Public domain W3C validator