Theorem lel 143

Description: Add conjunct to left of l.e.

Hypothesis

Ref	Expression
le.1	a =< b

Assertion

Ref	Expression
lel	(a ^ c) =< b

Proof of Theorem lel

Step	Hyp	Ref	Expression
1		an32 76	. . 3 ((a ^ c) ^ b) = ((a ^ b) ^ c)
2		le.1	. . . . 5 a =< b
3	2	df2le2 128	. . . 4 (a ^ b) = a
4	3	ran 71	. . 3 ((a ^ b) ^ c) = (a ^ c)
5	1, 4	ax-r2 35	. 2 ((a ^ c) ^ b) = (a ^ c)
6	5	df2le1 127	1 (a ^ c) =< b

Syntax hints:   =< wle 2   ^ wa 7

This theorem is referenced by:  negantlem9 841  neg3antlem2 847  marsdenlem3 864  cancellem 873

This theorem was proved from axioms:  ax-a1 29  ax-a2 30  ax-a3 31  ax-a5 33  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37

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

metamath.org