Theorem leran 153

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 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  1101  ml  1121  dp15lema  1152  dp15leme  1156  dp41lemh  1188  dp41leml  1191  xdp41  1196  xdp15  1197  xxdp41  1199  xxdp15  1200  xdp45lem  1202  xdp43lem  1203  xdp45  1204  xdp43  1205  3dp43  1206