Theorem df2le2 136

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

Hypothesis

Ref	Expression
df2le2.1	a =< b

Assertion

Ref	Expression
df2le2	(a ^ b) = a

Proof of Theorem df2le2

Step	Hyp	Ref	Expression
1		df2le2.1	. . 3 a =< b
2	1	df-le2 131	. 2 (a v b) = b
3	2	leoa 123	1 (a ^ b) = a

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

This theorem is referenced by:  lbtr 139  lel 151  leran 153  lecom 180  lei3 246  nom20 313  nom21 314  nom22 315  nom23 316  nom24 317  k1-8a 355  k1-4 359  wdf-c2 384  gsth 489  dfi3b 499  lem4 511  ud3lem1a 566  ud3lem1d 569  ud3lem3a 572  ud3lem3d 575  ud4lem1a 577  ud4lem1b 578  ud4lem3a 583  ud5lem1b 587  u3lemana 607  u4lemana 608  u4lemab 613  u5lemab 614  i1com 708  u4lem5 764  u4lem6 768  u24lem 770  u1lem8 776  u3lem15 795  bi1o1a 798  biao 799  imp3 841  mlaconj4 844  elimcons2 869  comanblem1 870  mhlem 876  mhlem1 877  mlaconjolem 885  e2ast2 894  e2astlem1 895  gomaex3lem9 922  oas 925  oagen1b 1015  oadistb 1020  oadistc0 1021  oadistc 1022  oadistd 1023  4oagen1b 1042  4oadist 1043  lem3.3.7i4e2 1069  lem3.3.7i5e1 1071

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-a 40  df-le2 131

Copyright terms: Public domain