Quantum Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  QLE Home  >  Th. List  >  fh4r GIF 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 ((ac) ∪ b) = ((ab) ∩ (cb))

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 ∪ (ac)) = ((ba) ∩ (bc))
4 ax-a2 31 . 2 ((ac) ∪ b) = (b ∪ (ac))
5 ax-a2 31 . . 3 (ab) = (ba)
6 ax-a2 31 . . 3 (cb) = (bc)
75, 62an 79 . 2 ((ab) ∩ (cb)) = ((ba) ∩ (bc))
83, 4, 73tr1 63 1 ((ac) ∪ b) = ((ab) ∩ (cb))
 Colors of variables: term Syntax hints:   = wb 1   C wc 3   ∪ 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