Theorem leid 148

Description: Identity law for "less than or equal to". (Contributed by NM, 24-Dec-1998.)

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  1088  lem4.6.6i0j2  1089  lem4.6.6i0j3  1090  lem4.6.6i0j4  1091  lem4.6.6i2j4  1097  lem4.6.6i3j0  1098  lem4.6.6i3j1  1099  lem4.6.6i4j2  1101  com3iia  1102  lem4.6.7  1103  mldual2i  1127  vneulem1  1131  vneulem13  1143  vneulemexp  1148  dp53lema  1163  dp35lem0  1179  xdp53  1200  xxdp53  1203  xdp43lem  1205  xdp43  1207  3dp43  1208