Theorem lelan 159

Description: Add conjunct to left of both sides

Hypothesis

Ref	Expression
lel.1	a =< b

Assertion

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

Proof of Theorem lelan

Step	Hyp	Ref	Expression
1		lel.1	. . 3 a =< b
2	1	leran 145	. 2 (a ^ c) =< (b ^ c)
3		ancom 68	. 2 (c ^ a) = (a ^ c)
4		ancom 68	. 2 (c ^ b) = (b ^ c)
5	2, 3, 4	le3tr1 132	1 (c ^ a) =< (c ^ b)

Syntax hints:   =< wle 2   ^ wa 7

This theorem is referenced by:  le2an 161  go1 335  i1or 337  i5lei3 341  wr5-2v 348  ortha 420  gsth 471  ud4lem1a 559  test 784  3vded11 796  mlaconj 827  elimconslem 849  elimcons 850  kb10iii 875  oas 905  oatr 908  oaur 910  oaidlem2 911  oaidlem2g 912  oa3to4lem1 925  oa3to4lem2 926  oa3to4lem3 927  oa4to6lem1 940  oa4to6lem2 941  oa4to6lem3 942  oa4to6lem4 943  oa4btoc 946  oa4uto4g 955  oa4uto4 957  oa3-1to5 973  oalem1 985  oadist2a 987  oagen1 994  oagen2 996  oadistc0 1001  oadistd 1003  4oagen1 1021  4oadist 1023

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