Theorem lerr 150

Description: Add disjunct to right of l.e. (Contributed by NM, 11-Nov-1997.)

Hypothesis

Ref	Expression
le.1	a ≤ b

Assertion

Ref	Expression
lerr	a ≤ (c ∪ b)

Proof of Theorem lerr

Step	Hyp	Ref	Expression
1		le.1	. . 3 a ≤ b
2	1	ler 149	. 2 a ≤ (b ∪ c)
3		ax-a2 31	. 2 (b ∪ c) = (c ∪ b)
4	2, 3	lbtr 139	1 a ≤ (c ∪ b)

Syntax hints:   ≤ wle 2   ∪ wo 6

This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  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:  ska2  432  i3orlem6  557  1oa  820  mhlem  876  marsdenlem3  882  cancellem  891  lem3.3.7i4e1  1069  lem4.6.6i2j1  1096  lem4.6.6i2j4  1097  lem4.6.6i3j1  1099  lem4.6.6i4j2  1101  vneulem6  1136  vneulemexp  1148  l42modlem1  1149  dp53lemc  1165  dp35lemc  1175  dp32  1196  xdp53  1200  xxdp53  1203  xdp43lem  1205  xdp43  1207  3dp43  1208  oadp35lemc  1211