Theorem lelor 166

Description: Add disjunct to left of both sides. (Contributed by NM, 25-Oct-1997.)

Hypothesis

Ref	Expression
lel.1	a ≤ b

Assertion

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

Proof of Theorem lelor

Step	Hyp	Ref	Expression
1		lel.1	. . 3 a ≤ b
2	1	leror 152	. 2 (a ∪ c) ≤ (b ∪ c)
3		ax-a2 31	. 2 (c ∪ a) = (a ∪ c)
4		ax-a2 31	. 2 (c ∪ b) = (b ∪ c)
5	2, 3, 4	le3tr1 140	1 (c ∪ 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-t 41  df-f 42  df-le1 130  df-le2 131

This theorem is referenced by:  le2or  168  ka4lemo  228  wlem1  243  wql1lem  287  nom14  311  nom20  313  nom21  314  nom22  315  go1  343  i2or  344  i1or  345  i5lei4  350  k1-8a  355  2vwomlem  365  wr5-2v  366  wdf-c2  384  ska2  432  ska4  433  i3or  497  i3orlem3  554  i2bi  722  u12lem  771  u3lem14mp  794  u3lemax4  796  u3lemax5  797  test2  803  3vded11  814  3vded22  818  sadm3  838  elimconslem  867  elimcons  868  govar2  897  oas  925  oat  927  oau  929  oa23  936  oa4lem1  937  oa4lem2  938  oa3to4lem1  945  oa3to4lem2  946  oa3to4lem3  947  oa4to6lem1  960  oa4to6lem2  961  oa4to6lem3  962  oa4to6lem4  963  oa4btoc  966  oa4uto4g  975  oa4uto4  977  oalem1  1005  mloa  1018  oadistc0  1021  lem3.3.5  1055  lem3.4.3  1076  lem4.6.6i0j1  1088  lem4.6.6i1j0  1092  lem4.6.6i1j3  1094  lem4.6.6i2j1  1096  ml3le  1129  dp15lema  1154  dp15leme  1158  dp53lema  1163  dp53lemf  1168  dp35lem0  1179  dp34  1181  dp41lemh  1190  xdp41  1198  xdp15  1199  xdp53  1200  xxdp41  1201  xxdp15  1202  xxdp53  1203  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208