Theorem ler 149

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 32	. . . 4 ((a v b) v c) = (a v (b v c))
2	1	ax-r1 35	. . 3 (a v (b v c)) = ((a v b) v c)
3		le.1	. . . . 5 a =< b
4	3	df-le2 131	. . . 4 (a v b) = b
5	4	ax-r5 38	. . 3 ((a v b) v c) = (b v c)
6	2, 5	ax-r2 36	. 2 (a v (b v c)) = (b v c)
7	6	df-le1 130	1 a =< (b v c)

Syntax hints:   =< wle 2   v wo 6

This theorem is referenced by:  lerr 150  i3orlem4 555  i3orlem7 558  i3orlem8 559  negantlem9 859  negantlem10 861  neg3antlem2 865  mhlemlem1 874  e2astlem1 895  lem3.4.3 1075  lem4.6.6i1j3 1091  lem4.6.6i2j1 1093  lem4.6.7 1100

This theorem was proved from axioms:  ax-a3 32  ax-r1 35  ax-r2 36  ax-r5 38

This theorem depends on definitions:  df-le1 130  df-le2 131

Copyright terms: Public domain