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

Theorem an1r 107
 Description: Conjunction with 1. (Contributed by NM, 26-Nov-1997.)
Assertion
Ref Expression
an1r (1 ∩ a) = a

Proof of Theorem an1r
StepHypRef Expression
1 ancom 74 . 2 (1 ∩ a) = (a ∩ 1)
2 an1 106 . 2 (a ∩ 1) = a
31, 2ax-r2 36 1 (1 ∩ a) = a
 Colors of variables: term Syntax hints:   = wb 1   ∩ wa 7  1wt 8 This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38 This theorem depends on definitions:  df-a 40  df-t 41  df-f 42 This theorem is referenced by:  ska2  432  ud3lem1c  568  ud3lem3  576  ud5lem1  589  i2i1i1  800  lem3.3.7i1e1  1060  lem3.3.7i1e2  1061  lem3.3.7i2e1  1063  lem3.3.7i2e2  1064  lem3.3.7i3e2  1067  lem3.3.7i4e2  1070  lem4.6.6i1j3  1094  dp15lema  1154  xdp15  1199  xxdp15  1202  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208
 Copyright terms: Public domain W3C validator