QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  fh4r Unicode version
Theorem fh4r 476
Description: Foulis-Holland Theorem.
Hypotheses
Ref Expression
fh.1 a C b
fh.2 a C c
Assertion
Ref Expression
fh4r ((a ^ c) v b) = ((a v b) ^ (c v b))
Proof of Theorem fh4r
StepHypRef Expression
1 fh.1 . . 3 a C b
2 fh.2 . . 3 a C c
31, 2fh4 472 . 2 (b v (a ^ c)) = ((b v a) ^ (b v c))
4 ax-a2 31 . 2 ((a ^ c) v b) = (b v (a ^ c))
5 ax-a2 31 . . 3 (a v b) = (b v a)
6 ax-a2 31 . . 3 (c v b) = (b v c)
75, 62an 79 . 2 ((a v b) ^ (c v b)) = ((b v a) ^ (b v c))
83, 4, 73tr1 63 1 ((a ^ c) v b) = ((a v b) ^ (c v b))
Colors of variables: term
Syntax hints:   = wb 1   C wc 3   v wo 6   ^ wa 7
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
This theorem is referenced by:  fh4rc  482  ud1lem1  560  ud1lem3  562  ud3lem1c  568  ud3lem3  576  ud4lem1c  579  ud4lem3  585  u4lemoa  623  u24lem  770  u3lem10  785  u3lem13a  789  u3lem13b  790  i1abs  801  test  802  test2  803
  Copyright terms: Public domain W3C validator