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

Theorem id 59
Description: Identity law.
Assertion
Ref Expression
id a = a

Proof of Theorem id
StepHypRef Expression
1 ax-a1 30 . 2 a = a''
21ax-r1 35 . 2 a'' = a
31, 2ax-r2 36 1 a = a
Colors of variables: term
Syntax hints:   = wb 1  'wn 4
This theorem is referenced by:  leid  148  str  189  mccune2  247  wql2lem4  291  nom10  307  ska2  432  woml7  437  u4lemana  608  u5lembi  725  u4lem1  737  u1lem3  749  u4lem6  768  u24lem  770  u12lem  771  u3lem11  786  u3lem13b  790  u3lem14a  791  mlaoml  833  mlaconj  845  neg3antlem2  865  mhlem  876  cancellem  891  gomaex3lem3  916  gomaex3  924  oa3to4lem6  950  oa4to6  965  oa3-2to2s  990  d3oa  995  d4oa  996  d6oa  997  mloa  1018  oa43v  1028  oa64v  1031  oa63v  1032  axoa4  1034  oa6  1036  axoa4a  1037  4oa  1039  dp15  1160  dp53  1168  dp35lem0  1177  dp35  1178  dp41  1193  xdp45lem  1202  xdp43lem  1203  xdp45  1204  xdp43  1205  3dp43  1206  oadp35  1210
This theorem was proved from axioms:  ax-a1 30  ax-r1 35  ax-r2 36
  Copyright terms: Public domain W3C validator