Theorem leor 151

Description: L.e. absorption.

Assertion

Ref	Expression
leor	a ≤ (b ∪ a)

Proof of Theorem leor

Step	Hyp	Ref	Expression
1		leo 150	. 2 a ≤ (a ∪ b)
2		ax-a2 30	. 2 (a ∪ b) = (b ∪ a)
3	1, 2	lbtr 131	1 a ≤ (b ∪ a)

Syntax hints:   ≤ wle 2   ∪ wo 6

This theorem is referenced by:  leao3 156  leao4 157  womao 212  womaon 213  womaa 214  womaan 215  anorabs2 216  anorabs 217  womle 290  nom20 305  i1or 337  i5lei3 341  ska2 414  i3th7 531  i3orlem1 534  i3orlem2 535  i3orlem3 536  i3orlem8 541  ud3lem1c 550  ud3lem1d 551  ud3lem3d 557  ud3lem3 558  ud4lem1b 560  ud4lem1 563  ud5lem1b 569  ud5lem1 571  u4lemona 610  u1lemob 612  u5lemob 616  i2bi 704  u4lem2 729  u4lem5 746  u4lem6 750  u24lem 752  i2i1i1 782  test 784  test2 785  3vth1 786  mlalem 814  sa5 818  negantlem9 841  negantlem10 843  neg3antlem2 847  elimcons2 851  comanblem1 852  mhlem 858  mh 861  mlaconjo 868  cancellem 873  gomaex3h7 888  gomaex3h11 892  gomaex3lem4 897  oat 907  oaidlem2 911  oaidlem2g 912  oa4lem2 918  oa4lem3 919  distoah3 922  oa3to4lem1 925  oa3to4lem2 926  oa4to6lem1 940  oa4to6lem2 941  oa4to6lem3 942  oa3-u1lem 965  d4oa 976  oadist2b 988  oagen1 994  oadist 999  oadistb 1000  oadistd 1003  oa4cl 1007  4oagen1 1021  4oadist 1023

This theorem was proved from axioms:  ax-a1 29  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  df-le2 123

metamath.org