Theorem leor 159

Description: L.e. absorption. (Contributed by NM, 11-Nov-1997.)

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  1089  lem4.6.6i2j0  1095  lem4.6.6i2j1  1096  lem4.6.6i2j4  1097  lem4.6.6i3j0  1098  lem4.6.6i4j2  1101  ml  1123  ml3le  1129  vneulem1  1131  vneulem6  1136  vneulemexp  1148  l42modlem2  1150  modexp  1152  dp53lema  1163  dp53lemb  1164  dp53lemd  1166  dp53lemg  1169  dp35leme  1173  dp35lemb  1176  dp41lemb  1183  dp41lemc0  1184  dp41leme  1187  dp41leml  1193  xdp41  1198  xdp53  1200  xxdp41  1201  xxdp53  1203  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208  testmod2  1215  testmod2expanded  1216  testmod3  1217