Theorem leor 159

Description: L.e. absorption.

Assertion

Ref	Expression
leor	a ≤ (b ∪ a)

Proof of Theorem leor

Step	Hyp	Ref	Expression
1		leo 158	. 2 a ≤ (a ∪ b)
2		ax-a2 31	. 2 (a ∪ b) = (b ∪ a)
3	1, 2	lbtr 139	1 a ≤ (b ∪ a)

Syntax hints:   ≤ wle 2   ∪ wo 6

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-le1 130  df-le2 131

This theorem is referenced by:  leao3  164  leao4  165  womao  220  womaon  221  womaa  222  womaan  223  anorabs2  224  womle  298  nom20  313  i1or  345  i5lei3  349  ska2  432  i3th7  549  i3orlem1  552  i3orlem2  553  i3orlem3  554  i3orlem8  559  ud3lem1c  568  ud3lem1d  569  ud3lem3d  575  ud3lem3  576  ud4lem1b  578  ud4lem1  581  ud5lem1b  587  ud5lem1  589  u4lemona  628  u1lemob  630  u5lemob  634  i2bi  722  u4lem2  747  u4lem5  764  u4lem6  768  u24lem  770  i2i1i1  800  test  802  test2  803  3vth1  804  mlalem  832  sa5  836  negantlem9  859  negantlem10  861  neg3antlem2  865  elimcons2  869  comanblem1  870  mhlem  876  mh  879  mlaconjo  886  cancellem  891  e2astlem1  895  gomaex3h7  908  gomaex3h11  912  gomaex3lem4  917  oat  927  oaidlem2  931  oaidlem2g  932  oa4lem2  938  oa4lem3  939  distoah3  942  oa3to4lem1  945  oa3to4lem2  946  oa4to6lem1  960  oa4to6lem2  961  oa4to6lem3  962  oa3-u1lem  985  d4oa  996  oadist2b  1008  oagen1  1014  oadist  1019  oadistb  1020  oadistd  1023  oa4cl  1027  4oagen1  1042  4oadist  1044  lem3.3.7i4e1  1069  lem4.6.6i0j2  1087  lem4.6.6i2j0  1093  lem4.6.6i2j1  1094  lem4.6.6i2j4  1095  lem4.6.6i3j0  1096  lem4.6.6i4j2  1099  ml  1121  ml3le  1127  vneulem1  1129  vneulem6  1134  vneulemexp  1146  l42modlem2  1148  modexp  1150  dp53lema  1161  dp53lemb  1162  dp53lemd  1164  dp53lemg  1167  dp35leme  1171  dp35lemb  1174  dp41lemb  1181  dp41lemc0  1182  dp41leme  1185  dp41leml  1191  xdp41  1196  xdp53  1198  xxdp41  1199  xxdp53  1201  xdp45lem  1202  xdp43lem  1203  xdp45  1204  xdp43  1205  3dp43  1206  testmod2  1213  testmod2expanded  1214  testmod3  1215