Theorem leid 140

Description: Identity law for less-than-or-equal.

Assertion

Ref	Expression
leid	a ≤ a

Proof of Theorem leid

Step	Hyp	Ref	Expression
1		id 58	. 2 a = a
2	1	bile 134	1 a ≤ a

Syntax hints:   ≤ wle 2

This theorem is referenced by:  bi1o1a 780  i2i1i1 782  1oa 802  negantlem2 831  mhlem 858  oago3.21x 872  gomaex3h6 887  gomaex3h9 890  gomaex3lem2 895  oaur 910  oa4btoc 946  oa3-u2lem 966  oa3-6to3 967  oa3-2to4 968  oa3-u1 971  oa3-1to5 973  d3oa 975  d4oa 976

This theorem was proved from axioms:  ax-a1 29  ax-a2 30  ax-a5 33  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37

This theorem depends on definitions:  df-t 40  df-f 41  df-le1 122

metamath.org