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 v c) =< (b v d)

Proof of Theorem le2or

Step	Hyp	Ref	Expression
1		le2.1	. . 3 a =< b
2	1	leror 152	. 2 (a v c) =< (b v c)
3		le2.2	. . 3 c =< d
4	3	lelor 166	. 2 (b v c) =< (b v d)
5	2, 4	letr 137	1 (a v c) =< (b v d)

Syntax hints:   =< wle 2   v wo 6

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 1043

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

Copyright terms: Public domain