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

Theorem fh1r 473
Description: Foulis-Holland Theorem. (Contributed by NM, 23-Nov-1997.)
Hypotheses
Ref Expression
fh.1 a C b
fh.2 a C c
Assertion
Ref Expression
fh1r ((bc) ∩ a) = ((ba) ∪ (ca))

Proof of Theorem fh1r
StepHypRef Expression
1 fh.1 . . 3 a C b
2 fh.2 . . 3 a C c
31, 2fh1 469 . 2 (a ∩ (bc)) = ((ab) ∪ (ac))
4 ancom 74 . 2 ((bc) ∩ a) = (a ∩ (bc))
5 ancom 74 . . 3 (ba) = (ab)
6 ancom 74 . . 3 (ca) = (ac)
75, 62or 72 . 2 ((ba) ∪ (ca)) = ((ab) ∪ (ac))
83, 4, 73tr1 63 1 ((bc) ∩ a) = ((ba) ∪ (ca))
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:  fh1rc  479  gsth  489  dfi3b  499  ud3lem1b  567  ud3lem1d  569  ud3lem3d  575  ud5lem1a  586  ud5lem3a  591  u1lemaa  600  u3lemaa  602  u4lemaa  603  u5lemaa  604  u3lemana  607  u4lemana  608  u5lemana  609  u3lemab  612  u4lemab  613  u5lemab  614  u2lemanb  616  u4lemanb  618  u5lemanb  619  u4lem4  759  u4lem5  764  u5lem5  765  u5lem6  769  u1lem8  776  u3lem15  795  bi1o1a  798  3vded21  817  1oa  820  neg3antlem2  865  mhlem  876  mhlem1  877  marsdenlem3  882  marsdenlem4  883
  Copyright terms: Public domain W3C validator