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 1069  lem3.3.7i4e2 1070  lem3.3.7i5e1 1072  lem4.6.6i0j1 1086  lem4.6.6i0j2 1087  lem4.6.6i0j3 1088  lem4.6.6i0j4 1089  lem4.6.6i2j4 1095  lem4.6.6i3j0 1096  lem4.6.6i3j1 1097  lem4.6.6i4j2 1099  com3iia 1100  lem4.6.7 1101  mldual2i 1125  vneulem1 1129  vneulem13 1141  vneulemexp 1146  dp53lema 1157

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