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 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

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  1161  dp35lem0  1177  xdp53  1198  xxdp53  1201  xdp43lem  1203  xdp43  1205  3dp43  1206