Theorem leran 153

Description: Add conjunct to right of both sides

Hypothesis

Ref	Expression
le.1	a =< b

Assertion

Ref	Expression
leran	(a ^ c) =< (b ^ c)

Proof of Theorem leran

Step	Hyp	Ref	Expression
1		anandir 115	. . . 4 ((a ^ b) ^ c) = ((a ^ c) ^ (b ^ c))
2	1	ax-r1 35	. . 3 ((a ^ c) ^ (b ^ c)) = ((a ^ b) ^ c)
3		le.1	. . . . 5 a =< b
4	3	df2le2 136	. . . 4 (a ^ b) = a
5	4	ran 78	. . 3 ((a ^ b) ^ c) = (a ^ c)
6	2, 5	ax-r2 36	. 2 ((a ^ c) ^ (b ^ c)) = (a ^ c)
7	6	df2le1 135	1 (a ^ c) =< (b ^ c)

Syntax hints:   =< wle 2   ^ wa 7

This theorem is referenced by:  lelan 167  le2an 169  i2or 344  i5lei4 350  k1-8a 355  3vth1 804  3vded21 817  3vded22 818  1oaiii 823  3vroa 831  eqtr4 834  sadm3 838  negantlem3 850  comanblem1 870  mh 879  gomaex4 900  oasr 926  oa3-u2lem 986  d4oa 996  oaliii 1001  oagen2b 1017  axoa4 1033  lem3.4.3 1075  lem4.6.7 1100

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