Theorem le2or 168

Description: Disjunction of 2 l.e.'s. (Contributed by NM, 25-Oct-1997.)

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 152	. 2 (a ∪ c) ≤ (b ∪ c)
3		le2.2	. . 3 c ≤ d
4	3	lelor 166	. 2 (b ∪ c) ≤ (b ∪ d)
5	2, 4	letr 137	1 (a ∪ c) ≤ (b ∪ d)

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:  lel2or  170  ler2or  172  ledi  174  ledio  176  ska15  244  id5leid0  351  ska2  432  ka4ot  435  i3bi  496  lem4  511  binr3  519  i3th5  547  3vcom  813  3vded22  818  sadm3  838  mlaconjo  886  govar  896  distoa  944  oa3to4lem3  947  oa4to6lem4  963  oa4uto4g  975  oa4uto4  977  oa3-u2lem  986  d3oa  995  oadistd  1023  4oadist  1044  dp15lemf  1159  dp35lemd  1174  dp41lemh  1190  dp41leml  1193  xdp41  1198  xdp15  1199  xxdp41  1201  xxdp15  1202  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208