Theorem leran 145

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 107	. . . 4 ((a ^ b) ^ c) = ((a ^ c) ^ (b ^ c))
2	1	ax-r1 34	. . 3 ((a ^ c) ^ (b ^ c)) = ((a ^ b) ^ c)
3		le.1	. . . . 5 a =< b
4	3	df2le2 128	. . . 4 (a ^ b) = a
5	4	ran 71	. . 3 ((a ^ b) ^ c) = (a ^ c)
6	2, 5	ax-r2 35	. 2 ((a ^ c) ^ (b ^ c)) = (a ^ c)
7	6	df2le1 127	1 (a ^ c) =< (b ^ c)

Syntax hints:   =< wle 2   ^ wa 7

This theorem is referenced by:  lelan 159  le2an 161  i2or 336  i5lei4 342  3vth1 786  3vded21 799  3vded22 800  1oaiii 805  3vroa 813  eqtr4 816  sadm3 820  negantlem3 832  comanblem1 852  mh 861  gomaex4 880  oasr 906  oa3-u2lem 966  d4oa 976  oaliii 981  oagen2b 997  axoa4 1013

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-t 40  df-f 41  df-le1 122  df-le2 123

metamath.org