Theorem id 59

Description: Identity law. (Contributed by NM, 9-Aug-1997.)

Assertion

Ref	Expression
id	a = a

Proof of Theorem id

Step	Hyp	Ref	Expression
1		ax-a1 30	. 2 a = a⊥ ⊥
2	1	ax-r1 35	. 2 a⊥ ⊥ = a
3	1, 2	ax-r2 36	1 a = a

Syntax hints:   = wb 1  ^⊥ wn 4

This theorem was proved from axioms:  ax-a1 30  ax-r1 35  ax-r2 36

This theorem is referenced by:  leid  148  str  189  mccune2  247  wql2lem4  291  nom10  307  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  1162  dp53  1170  dp35lem0  1179  dp35  1180  dp41  1195  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208  oadp35  1212