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 142  str 183  mccune2 241  wql2lem4 285  nom10 301  ska2 418  woml7 423  u4lemana 594  u5lembi 711  u4lem1 723  u1lem3 735  u4lem6 754  u24lem 756  u12lem 757  u3lem11 772  u3lem13b 776  u3lem14a 777  mlaoml 819  mlaconj 831  neg3antlem2 851  mhlem 862  cancellem 877  gomaex3lem3 902  gomaex3 910  oa3to4lem6 936  oa4to6 951  oa3-2to2s 976  d3oa 981  d4oa 982  d6oa 983  mloa 1004  oa43v 1014  oa64v 1016  oa63v 1017  axoa4 1019  oa6 1021  axoa4a 1022  4oa 1024

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

Copyright terms: Public domain