Theorem ler2an 165

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 103	. . 3 (a ^ a) = a
2	1	ax-r1 34	. 2 a = (a ^ a)
3		ler2.1	. . 3 a =< b
4		ler2.2	. . 3 a =< c
5	3, 4	le2an 161	. 2 (a ^ a) =< (b ^ c)
6	2, 5	bltr 130	1 a =< (b ^ c)

Syntax hints:   =< wle 2   ^ wa 7

This theorem is referenced by:  distlem 180  str 181  womao 212  womaon 213  womaa 214  womaan 215  anorabs2 216  anorabs 217  mccune2 239  oaidlem1 286  nom14 303  2vwomlem 347  ska4 415  i3orlem7 540  ud3lem1a 548  ud4lem1b 560  ud5lem1b 569  bi1o1a 780  biao 781  i2i1i1 782  3vth2 787  3vth6 791  3vded21 799  oaeqv 812  mlaconj4 826  negantlem2 831  negantlem9 841  negantlem10 843  neg3antlem2 847  mhlem 858  mhlem2 860  mh 861  distid 869  oago3.21x 872  cancellem 873  govar2 877  gon2n 878  gomaex4 880  oas 905  oat 907  oau 909  oa23 916  oa4lem1 917  oa4lem2 918  oaliv 983  oagen1 994  4oaiii 1019  4oagen1 1021

This theorem was proved from axioms:  ax-a1 29  ax-a2 30  ax-a3 31  ax-a5 33  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37

This theorem depends on definitions:  df-a 39  df-t 40  df-f 41  df-le1 122  df-le2 123

metamath.org