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  1086  lem4.6.6i1j0  1090  lem4.6.6i1j3  1092  lem4.6.6i2j1  1094  ml3le  1127  dp15lema  1152  dp15leme  1156  dp53lema  1161  dp53lemf  1166  dp35lem0  1177  dp34  1179  dp41lemh  1188  xdp41  1196  xdp15  1197  xdp53  1198  xxdp41  1199  xxdp15  1200  xxdp53  1201  xdp45lem  1202  xdp43lem  1203  xdp45  1204  xdp43  1205  3dp43  1206