Theorem id 59

Description: Identity law.

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 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 1030  oa63v 1031  axoa4 1033  oa6 1035  axoa4a 1036  4oa 1038

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

Copyright terms: Public domain