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

Theorem an4 86
Description: Swap conjuncts. (Contributed by NM, 27-Aug-1997.)
Assertion
Ref Expression
an4 ((ab) ∩ (cd)) = ((ac) ∩ (bd))

Proof of Theorem an4
StepHypRef Expression
1 an12 81 . . 3 (b ∩ (cd)) = (c ∩ (bd))
21lan 77 . 2 (a ∩ (b ∩ (cd))) = (a ∩ (c ∩ (bd)))
3 anass 76 . 2 ((ab) ∩ (cd)) = (a ∩ (b ∩ (cd)))
4 anass 76 . 2 ((ac) ∩ (bd)) = (a ∩ (c ∩ (bd)))
52, 3, 43tr1 63 1 ((ab) ∩ (cd)) = ((ac) ∩ (bd))
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:  anandi  114  anandir  115  wwfh2  217  wfh2  424  fh2  470  gsth  489  i3bi  496  ud4lem1a  577  ud5lem1c  588  ud5lem3a  591  ud5lem3c  593  u5lembi  725  u3lem13b  790  3vth7  810  mlalem  832  bi3  839  bi4  840  mlaconj4  844  comanblem1  870  comanblem2  871  mhlem  876  mh  879  marsdenlem3  882  marsdenlem4  883  mhcor1  888  gomaex4  900  gomaex3lem8  921  vneulem16  1146  vneulemexp  1148
  Copyright terms: Public domain W3C validator