Theorem id 58

Description: Identity law.

Assertion

Ref	Expression
id	a = a

Proof of Theorem id

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

Syntax hints:   = wb 1  ^⊥ wn 4

This theorem is referenced by:  leid 140  str 181  mccune2 239  wql2lem4 283  nom10 299  ska2 414  woml7 419  u4lemana 590  u5lembi 707  u4lem1 719  u1lem3 731  u4lem6 750  u24lem 752  u12lem 753  u3lem11 768  u3lem13b 772  u3lem14a 773  mlaoml 815  mlaconj 827  neg3antlem2 847  mhlem 858  cancellem 873  gomaex3lem3 896  gomaex3 904  oa3to4lem6 930  oa4to6 945  oa3-2to2s 970  d3oa 975  d4oa 976  d6oa 977  mloa 998  oa43v 1008  oa64v 1010  oa63v 1011  axoa4 1013  oa6 1015  axoa4a 1016  4oa 1018

This theorem was proved from axioms:  ax-a1 29  ax-r1 34  ax-r2 35

metamath.org