Theorem df2le1 135

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 124	. 2 (a v b) = b
3	2	df-le1 130	1 a =< b

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

This theorem is referenced by:  letr 137  lbtr 139  lel 151  leran 153  lecon 154  leo 158  i3le 515  u1lemle2 715  u2lemle2 716  u4lemle2 718  u5lemle2 719  bi4 840  gomaex3lem2 915

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

This theorem depends on definitions:  df-a 40  df-le1 130

Copyright terms: Public domain