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 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  4oaiii 1039  4oagen1 1041  lem3.3.3lem3 1050  lem3.3.7i4e1 1068  lem3.3.7i4e2 1069  lem3.3.7i5e1 1071  lem3.4.3 1075  com3iia 1099  lem4.6.7 1100

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

Copyright terms: Public domain