Theorem ler 141

Description: Add disjunct to right of l.e.

Hypothesis

Ref	Expression
le.1	a =< b

Assertion

Ref	Expression
ler	a =< (b v c)

Proof of Theorem ler

Step	Hyp	Ref	Expression
1		ax-a3 31	. . . 4 ((a v b) v c) = (a v (b v c))
2	1	ax-r1 34	. . 3 (a v (b v c)) = ((a v b) v c)
3		le.1	. . . . 5 a =< b
4	3	df-le2 123	. . . 4 (a v b) = b
5	4	ax-r5 37	. . 3 ((a v b) v c) = (b v c)
6	2, 5	ax-r2 35	. 2 (a v (b v c)) = (b v c)
7	6	df-le1 122	1 a =< (b v c)

Syntax hints:   =< wle 2   v wo 6

This theorem is referenced by:  lerr 142  i3orlem4 537  i3orlem7 540  i3orlem8 541  negantlem9 841  negantlem10 843  neg3antlem2 847  mhlemlem1 856

This theorem was proved from axioms:  ax-a3 31  ax-r1 34  ax-r2 35  ax-r5 37

This theorem depends on definitions:  df-le1 122  df-le2 123

metamath.org