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

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

Proof of Theorem fh3
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, 4fh1 469 . . 3 (a' ^ (b' v c')) = ((a' ^ b') v (a' ^ c'))
6 anor2 89 . . . 4 (a' ^ (b' v c')) = (a v (b' v c')')'
7 df-a 40 . . . . . . 7 (b ^ c) = (b' v c')'
87ax-r1 35 . . . . . 6 (b' v c')' = (b ^ c)
98lor 70 . . . . 5 (a v (b' v c')') = (a v (b ^ c))
109ax-r4 37 . . . 4 (a v (b' v c')')' = (a v (b ^ c))'
116, 10ax-r2 36 . . 3 (a' ^ (b' v c')) = (a v (b ^ c))'
12 oran 87 . . . 4 ((a' ^ b') v (a' ^ c')) = ((a' ^ b')' ^ (a' ^ c')')'
13 oran 87 . . . . . . 7 (a v b) = (a' ^ b')'
14 oran 87 . . . . . . 7 (a v c) = (a' ^ c')'
1513, 142an 79 . . . . . 6 ((a v b) ^ (a v c)) = ((a' ^ b')' ^ (a' ^ c')')
1615ax-r1 35 . . . . 5 ((a' ^ b')' ^ (a' ^ c')') = ((a v b) ^ (a v c))
1716ax-r4 37 . . . 4 ((a' ^ b')' ^ (a' ^ c')')' = ((a v b) ^ (a v c))'
1812, 17ax-r2 36 . . 3 ((a' ^ b') v (a' ^ c')) = ((a v b) ^ (a v c))'
195, 11, 183tr2 64 . 2 (a v (b ^ c))' = ((a v b) ^ (a v c))'
2019con1 66 1 (a v (b ^ c)) = ((a v b) ^ (a 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:  fh3r  475  i3bi  496  oi3ai3  503  ud1lem2  561  ud1lem3  562  ud2lem3  565  ud3lem1  570  ud4lem1a  577  ud5lem3  594  u4lemob  633  u1lembi  720  u4lem4  759  test  802  3vth5  808  3vth7  810  3vth9  812  1oa  820  2oalem1  825  neg3antlem2  865  comanblem1  870  mhlem  876  gomaex3lem1  914  oau  929  oa23  936  oa3to4lem1  945  oa3to4lem2  946  oa4to6lem1  960  oa4to6lem2  961  oa4to6lem3  962  oa3moa3  1029  lem4.6.2e1  1080  lem4.6.6i1j3  1092  com3iia  1100  lem4.6.7  1101
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