Theorem leid 148

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

Assertion

Ref	Expression
leid	a =< a

Proof of Theorem leid

Step	Hyp	Ref	Expression
1		id 59	. 2 a = a
2	1	bile 142	1 a =< a

Syntax hints:   =< wle 2

This theorem is referenced by:  bi1o1a 798  i2i1i1 800  1oa 820  negantlem2 849  mhlem 876  oago3.21x 890  gomaex3h6 907  gomaex3h9 910  gomaex3lem2 915  oaur 930  oa4btoc 966  oa3-u2lem 986  oa3-6to3 987  oa3-2to4 988  oa3-u1 991  oa3-1to5 993  d3oa 995  d4oa 996  lem3.3.7i4e1 1068  lem3.3.7i4e2 1069  lem3.3.7i5e1 1071  lem4.6.6i0j1 1085  lem4.6.6i0j2 1086  lem4.6.6i0j3 1087  lem4.6.6i0j4 1088  lem4.6.6i2j4 1094  lem4.6.6i3j0 1095  lem4.6.6i3j1 1096  lem4.6.6i4j2 1098  com3iia 1099  lem4.6.7 1100

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

This theorem depends on definitions:  df-t 41  df-f 42  df-le1 130

Copyright terms: Public domain