Theorem lelan 167

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 153	. 2 (a ^ c) =< (b ^ c)
3		ancom 74	. 2 (c ^ a) = (a ^ c)
4		ancom 74	. 2 (c ^ b) = (b ^ c)
5	2, 3, 4	le3tr1 140	1 (c ^ a) =< (c ^ b)

Syntax hints:   =< wle 2   ^ wa 7

This theorem is referenced by:  le2an 169  go1 343  i1or 345  i5lei3 349  wr5-2v 366  ortha 438  gsth 489  ud4lem1a 577  test 802  3vded11 814  mlaconj 845  elimconslem 867  elimcons 868  kb10iii 893  oas 925  oatr 928  oaur 930  oaidlem2 931  oaidlem2g 932  oa3to4lem1 945  oa3to4lem2 946  oa3to4lem3 947  oa4to6lem1 960  oa4to6lem2 961  oa4to6lem3 962  oa4to6lem4 963  oa4btoc 966  oa4uto4g 975  oa4uto4 977  oa3-1to5 993  oalem1 1005  oadist2a 1007  oagen1 1014  oagen2 1016  oadistc0 1021  oadistd 1023  4oagen1 1041  4oadist 1043  lem3.3.5 1054

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