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

Theorem fh2r 474
 Description: Foulis-Holland Theorem.
Hypotheses
Ref Expression
fh.1 a C b
fh.2 a C c
Assertion
Ref Expression
fh2r ((ac) ∩ b) = ((ab) ∪ (cb))

Proof of Theorem fh2r
StepHypRef Expression
1 fh.1 . . 3 a C b
2 fh.2 . . 3 a C c
31, 2fh2 470 . 2 (b ∩ (ac)) = ((ba) ∪ (bc))
4 ancom 74 . 2 ((ac) ∩ b) = (b ∩ (ac))
5 ancom 74 . . 3 (ab) = (ba)
6 ancom 74 . . 3 (cb) = (bc)
75, 62or 72 . 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:  fh2rc  480  ud3lem1a  566  ud3lem2  571  ud3lem3d  575  ud4lem1a  577  ud4lem1b  578  u2lemaa  601  u4lemaa  603  u2lemana  606  u4lemana  608  u1lemab  610  u3lemab  612  u1lemanb  615  u3lemanb  617  u4lemc4  704  u5lemc4  705  u4lem4  759  u24lem  770  bi3  839  bi4  840  marsdenlem1  880  e2astlem1  895  govar  896
 Copyright terms: Public domain W3C validator