Theorem df2le1 127

Description: Alternate definition of 'less than or equal to'.

Hypothesis

Ref	Expression
df2le1.1	(a ^ b) = a

Assertion

Ref	Expression
df2le1	a =< b

Proof of Theorem df2le1

Step	Hyp	Ref	Expression
1		df2le1.1	. . 3 (a ^ b) = a
2	1	leao 116	. 2 (a v b) = b
3	2	df-le1 122	1 a =< b

Syntax hints:   = wb 1   =< wle 2   ^ wa 7

This theorem is referenced by:  letr 129  lbtr 131  lel 143  leran 145  lecon 146  leo 150  i3le 497  u1lemle2 697  u2lemle2 698  u4lemle2 700  u5lemle2 701  bi4 822  gomaex3lem2 895

This theorem was proved from axioms:  ax-a2 30  ax-a5 33  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37

This theorem depends on definitions:  df-a 39  df-le1 122

metamath.org