Theorem leran 153

Description: Add conjunct to right of both sides. (Contributed by NM, 27-Aug-1997.)

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 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:  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  1034  lem3.4.3  1076  lem4.6.7  1103  ml  1123  dp15lema  1154  dp15leme  1158  dp41lemh  1190  dp41leml  1193  xdp41  1198  xdp15  1199  xxdp41  1201  xxdp15  1202  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208