Theorem ler2an 173

Description: Conjunction of 2 l.e.'s.

Hypotheses

Ref	Expression
ler2.1	a ≤ b
ler2.2	a ≤ c

Assertion

Ref	Expression
ler2an	a ≤ (b ∩ c)

Proof of Theorem ler2an

Step	Hyp	Ref	Expression
1		anidm 111	. . 3 (a ∩ a) = a
2	1	ax-r1 35	. 2 a = (a ∩ a)
3		ler2.1	. . 3 a ≤ b
4		ler2.2	. . 3 a ≤ c
5	3, 4	le2an 169	. 2 (a ∩ a) ≤ (b ∩ c)
6	2, 5	bltr 138	1 a ≤ (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:  distlem  188  str  189  womao  220  womaon  221  womaa  222  womaan  223  anorabs2  224  mccune2  247  oaidlem1  294  nom14  311  id5leid0  351  k1-8a  355  2vwomlem  365  ska4  433  i3orlem7  558  ud3lem1a  566  ud4lem1b  578  ud5lem1b  587  bi1o1a  798  biao  799  i2i1i1  800  3vth2  805  3vth6  809  3vded21  817  oaeqv  830  mlaconj4  844  negantlem2  849  negantlem9  859  negantlem10  861  neg3antlem2  865  mhlem  876  mhlem2  878  mh  879  distid  887  oago3.21x  890  cancellem  891  govar2  897  gon2n  898  gomaex4  900  oas  925  oat  927  oau  929  oa23  936  oa4lem1  937  oa4lem2  938  oaliv  1003  oagen1  1014  oa3moa3  1029  4oaiii  1040  4oagen1  1042  lem3.3.3lem3  1051  lem3.3.7i4e1  1069  lem3.3.7i4e2  1070  lem3.3.7i5e1  1072  lem3.4.3  1076  com3iia  1100  lem4.6.7  1101  ml  1121  mldual2i  1125  ml3le  1127  vneulem1  1129  vneulem6  1134  vneulem7  1135  vneulem13  1141  vneulemexp  1146  dp53lema  1161  dp53lemc  1163  dp53lemd  1164  dp53lemf  1166  dp35lemd  1172  dp35lemc  1173  dp41lemh  1188  dp32  1194  xdp41  1196  xdp53  1198  xxdp41  1199  xxdp53  1201  xdp45lem  1202  xdp43lem  1203  xdp45  1204  xdp43  1205  3dp43  1206  oadp35lemc  1209  testmod2  1213  testmod2expanded  1214