Theorem ler 149

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

Hypothesis

Ref	Expression
le.1	a ≤ b

Assertion

Ref	Expression
ler	a ≤ (b ∪ c)

Proof of Theorem ler

Step	Hyp	Ref	Expression
1		ax-a3 32	. . . 4 ((a ∪ b) ∪ c) = (a ∪ (b ∪ c))
2	1	ax-r1 35	. . 3 (a ∪ (b ∪ c)) = ((a ∪ b) ∪ c)
3		le.1	. . . . 5 a ≤ b
4	3	df-le2 131	. . . 4 (a ∪ b) = b
5	4	ax-r5 38	. . 3 ((a ∪ b) ∪ c) = (b ∪ c)
6	2, 5	ax-r2 36	. 2 (a ∪ (b ∪ c)) = (b ∪ c)
7	6	df-le1 130	1 a ≤ (b ∪ c)

Syntax hints:   ≤ wle 2   ∪ wo 6

This theorem was proved from axioms:  ax-a3 32  ax-r1 35  ax-r2 36  ax-r5 38

This theorem depends on definitions:  df-le1 130  df-le2 131

This theorem is referenced by:  lerr  150  i3orlem4  555  i3orlem7  558  i3orlem8  559  negantlem9  859  negantlem10  861  neg3antlem2  865  mhlemlem1  874  e2astlem1  895  lem3.4.3  1076  lem4.6.6i1j3  1094  lem4.6.6i2j1  1096  lem4.6.7  1103  vneulem6  1136  vneulemexp  1148  dp41lemc0  1184  xdp41  1198  xxdp41  1201  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208  testmod2  1215  testmod2expanded  1216  testmod3  1217