Theorem lelor 158

Description: Add disjunct to left of both sides

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 144	. 2 (a ∪ c) ≤ (b ∪ c)
3		ax-a2 30	. 2 (c ∪ a) = (a ∪ c)
4		ax-a2 30	. 2 (c ∪ b) = (b ∪ c)
5	2, 3, 4	le3tr1 132	1 (c ∪ a) ≤ (c ∪ b)

Syntax hints:   ≤ wle 2   ∪ wo 6

This theorem is referenced by:  le2or 160  ka4lemo 220  wlem1 235  wql1lem 279  nom14 303  nom20 305  nom21 306  nom22 307  go1 335  i2or 336  i1or 337  i5lei4 342  2vwomlem 347  wr5-2v 348  wdf-c2 366  ska2 414  ska4 415  i3or 479  i3orlem3 536  i2bi 704  u12lem 753  u3lem14mp 776  u3lemax4 778  u3lemax5 779  test2 785  3vded11 796  3vded22 800  sadm3 820  elimconslem 849  elimcons 850  govar2 877  oas 905  oat 907  oau 909  oa23 916  oa4lem1 917  oa4lem2 918  oa3to4lem1 925  oa3to4lem2 926  oa3to4lem3 927  oa4to6lem1 940  oa4to6lem2 941  oa4to6lem3 942  oa4to6lem4 943  oa4btoc 946  oa4uto4g 955  oa4uto4 957  oalem1 985  mloa 998  oadistc0 1001

This theorem was proved from axioms:  ax-a1 29  ax-a2 30  ax-a3 31  ax-a5 33  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37

This theorem depends on definitions:  df-a 39  df-t 40  df-f 41  df-le1 122  df-le2 123

metamath.org