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

Theorem an12 81
 Description: Swap conjuncts.
Assertion
Ref Expression
an12 (a ∩ (bc)) = (b ∩ (ac))

Proof of Theorem an12
StepHypRef Expression
1 ancom 74 . . 3 (ab) = (ba)
21ran 78 . 2 ((ab) ∩ c) = ((ba) ∩ c)
3 anass 76 . 2 ((ab) ∩ c) = (a ∩ (bc))
4 anass 76 . 2 ((ba) ∩ c) = (b ∩ (ac))
52, 3, 43tr2 64 1 (a ∩ (bc)) = (b ∩ (ac))
 Colors of variables: term Syntax hints:   = wb 1   ∩ wa 7 This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38 This theorem depends on definitions:  df-a 40 This theorem is referenced by:  an4  86  wwfh1  216  wwfh2  217  wfh1  423  wfh2  424  oml5a  450  fh1  469  fh2  470  i3bi  496  dfi3b  499  ud3lem1b  567  ud4lem1a  577  ud4lem1b  578  ud4lem1d  580  ud5lem1a  586  u4lemle2  718  u12lembi  726  u2lem8  782  1oa  820  mlalem  832  mlaoml  833  bi3  839  bi4  840  mlaconjo  886  cancellem  891  gomaex3lem9  922  testmod  1211
 Copyright terms: Public domain W3C validator