Theorem lerr 150

Description: Add disjunct to right of l.e.

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:  i3orlem6  557  1oa  820  mhlem  876  marsdenlem3  882  cancellem  891  lem3.3.7i4e1  1069  lem4.6.6i2j1  1094  lem4.6.6i2j4  1095  lem4.6.6i3j1  1097  lem4.6.6i4j2  1099  vneulem6  1134  vneulemexp  1146  l42modlem1  1147  dp53lemc  1163  dp35lemc  1173  dp32  1194  xdp53  1198  xxdp53  1201  xdp43lem  1203  xdp43  1205  3dp43  1206  oadp35lemc  1209