Theorem le1 138

Description: Anything is l.e. 1.

Assertion

Ref	Expression
le1	a ≤ 1

Proof of Theorem le1

Step	Hyp	Ref	Expression
1		or1 96	. 2 (a ∪ 1) = 1
2	1	df-le1 122	1 a ≤ 1

Syntax hints:   ≤ wle 2  1wt 9

This theorem is referenced by:  ka4lemo 220  wlem1 235  bina5 278  wql1lem 279  wql2lem 280  womle2a 287  womle2b 288  womle3b 289  nom23 308  2vwomlem 347  wr5-2v 348  wom3 349  wdf-c2 366  ska2 414  ska4 415  wom2 416  ka4ot 417  cmtr1com 475  i3or 479  u3lemax4 778  u3lemax5 779  3vded11 796  3vded12 797  3vroa 813  oa3-2to4 968  oa3-u1 971  oa3-u2 972

This theorem was proved from axioms:  ax-a2 30  ax-a4 32  ax-r1 34  ax-r2 35  ax-r5 37

This theorem depends on definitions:  df-t 40  df-le1 122

metamath.org