Theorem leror 152

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

Hypothesis

Ref	Expression
le.1	a ≤ b

Assertion

Ref	Expression
leror	(a ∪ c) ≤ (b ∪ c)

Proof of Theorem leror

Step	Hyp	Ref	Expression
1		orordir 113	. . . 4 ((a ∪ b) ∪ c) = ((a ∪ c) ∪ (b ∪ c))
2	1	ax-r1 35	. . 3 ((a ∪ c) ∪ (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 ∪ c) ∪ (b ∪ c)) = (b ∪ c)
7	6	df-le1 130	1 (a ∪ c) ≤ (b ∪ c)

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-t 41  df-f 42  df-le1 130  df-le2 131

This theorem is referenced by:  lelor  166  le2or  168  ka4lemo  228  ska13  241  wql2lem  288  womle2a  295  nom24  317  i5lei1  347  i5lei2  348  i5lei3  349  ska2  432  ska4  433  ka4ot  435  cmtr1com  493  ud4lem3a  583  ud4lem3b  584  comi1  709  3vded21  817  3vded22  818  3vroa  831  sa5  836  negantlem2  849  negantlem3  850  negantlem9  859  elimconslem  867  elimcons  868  comanb  872  e2ast2  894  oa4uto4g  975  oagen1  1014  4oagen1  1042  lem3.3.3lem1  1049  lem3.3.3lem2  1050  vneulem6  1136  vneulemexp  1148  l42modlem2  1150  dp15lema  1154  dp15lemf  1159  dp53leme  1167  dp41lemb  1183  dp41leme  1187  dp23  1197  xdp41  1198  xdp15  1199  xdp53  1200  xxdp41  1201  xxdp15  1202  xxdp53  1203  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208  testmod2  1215  testmod2expanded  1216