Theorem ler2an 173

Description: Conjunction of 2 l.e.'s. (Contributed by NM, 11-Nov-1997.)

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  1102  lem4.6.7  1103  ml  1123  mldual2i  1127  ml3le  1129  vneulem1  1131  vneulem6  1136  vneulem7  1137  vneulem13  1143  vneulemexp  1148  dp53lema  1163  dp53lemc  1165  dp53lemd  1166  dp53lemf  1168  dp35lemd  1174  dp35lemc  1175  dp41lemh  1190  dp32  1196  xdp41  1198  xdp53  1200  xxdp41  1201  xxdp53  1203  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208  oadp35lemc  1211  testmod2  1215  testmod2expanded  1216