Theorem lerr 150

Description: Add disjunct to right of l.e.

Hypothesis

Ref	Expression
le.1	a =< b

Assertion

Ref	Expression
lerr	a =< (c v b)

Proof of Theorem lerr

Step	Hyp	Ref	Expression
1		le.1	. . 3 a =< b
2	1	ler 149	. 2 a =< (b v c)
3		ax-a2 31	. 2 (b v c) = (c v b)
4	2, 3	lbtr 139	1 a =< (c v b)

Syntax hints:   =< wle 2   v wo 6

This theorem is referenced by:  i3orlem6 557  1oa 820  mhlem 876  marsdenlem3 882  cancellem 891  lem3.3.7i4e1 1068  lem4.6.6i2j1 1093  lem4.6.6i2j4 1094  lem4.6.6i3j1 1096  lem4.6.6i4j2 1098

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-le1 130  df-le2 131

Copyright terms: Public domain