Theorem ler 149

Description: Add disjunct to right of l.e.

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  1092  lem4.6.6i2j1  1094  lem4.6.7  1101  vneulem6  1134  vneulemexp  1146  dp41lemc0  1182  xdp41  1196  xxdp41  1199  xdp45lem  1202  xdp43lem  1203  xdp45  1204  xdp43  1205  3dp43  1206  testmod2  1213  testmod2expanded  1214  testmod3  1215