Theorem le2or 160

Description: Disjunction of 2 l.e.'s

Hypotheses

Ref	Expression
le2.1	a ≤ b
le2.2	c ≤ d

Assertion

Ref	Expression
le2or	(a ∪ c) ≤ (b ∪ d)

Proof of Theorem le2or

Step	Hyp	Ref	Expression
1		le2.1	. . 3 a ≤ b
2	1	leror 144	. 2 (a ∪ c) ≤ (b ∪ c)
3		le2.2	. . 3 c ≤ d
4	3	lelor 158	. 2 (b ∪ c) ≤ (b ∪ d)
5	2, 4	letr 129	1 (a ∪ c) ≤ (b ∪ d)

Syntax hints:   ≤ wle 2   ∪ wo 6

This theorem is referenced by:  lel2or 162  ler2or 164  ledi 166  ledio 168  ska15 236  wr5 413  ska2 414  ka4ot 417  i3bi 478  lem4 493  binr3 501  i3th5 529  3vcom 795  3vded22 800  sadm3 820  mlaconjo 868  govar 876  distoa 924  oa3to4lem3 927  oa4to6lem4 943  oa4uto4g 955  oa4uto4 957  oa3-u2lem 966  d3oa 975  oadistd 1003  4oadist 1023

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