Theorem le2or 168

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 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  1157  dp35lemd  1172  dp41lemh  1188  dp41leml  1191  xdp41  1196  xdp15  1197  xxdp41  1199  xxdp15  1200  xdp45lem  1202  xdp43lem  1203  xdp45  1204  xdp43  1205  3dp43  1206