Theorem lelan 167

Description: Add conjunct to left of both sides. (Contributed by NM, 25-Oct-1997.)

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 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

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  1042  4oadist  1044  lem3.3.5  1055  dp15lemf  1159  dp35lem0  1179  dp41lemc  1185  dp41lemh  1190  dp41leml  1193  xdp41  1198  xdp15  1199  xxdp41  1201  xxdp15  1202  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208