Theorem le1 146

Description: Anything is l.e. 1.

Assertion

Ref	Expression
le1	a =< 1

Proof of Theorem le1

Step	Hyp	Ref	Expression
1		or1 104	. 2 (a v 1) = 1
2	1	df-le1 130	1 a =< 1

Syntax hints:   =< wle 2  1wt 8

This theorem is referenced by:  ka4lemo 228  wlem1 243  bina5 286  wql1lem 287  wql2lem 288  womle2a 295  womle2b 296  womle3b 297  nom23 316  2vwomlem 365  wr5-2v 366  wom3 367  wdf-c2 384  ska2 432  ska4 433  wom2 434  ka4ot 435  cmtr1com 493  i3or 497  u3lemax4 796  u3lemax5 797  3vded11 814  3vded12 815  3vroa 831  oa3-2to4 988  oa3-u1 991  oa3-u2 992  lem3.3.5lem 1053  lem4.6.7 1100  wdwom 1103

This theorem was proved from axioms:  ax-a2 31  ax-a4 33  ax-r1 35  ax-r2 36  ax-r5 38

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

Copyright terms: Public domain