Theorem le2an 161

Description: Conjunction of 2 l.e.'s

Hypotheses

Ref	Expression
le2.1	a =< b
le2.2	c =< d

Assertion

Ref	Expression
le2an	(a ^ c) =< (b ^ d)

Proof of Theorem le2an

Step	Hyp	Ref	Expression
1		le2.1	. . 3 a =< b
2	1	leran 145	. 2 (a ^ c) =< (b ^ c)
3		le2.2	. . 3 c =< d
4	3	lelan 159	. 2 (b ^ c) =< (b ^ d)
5	2, 4	letr 129	1 (a ^ c) =< (b ^ d)

Syntax hints:   =< wle 2   ^ wa 7

This theorem is referenced by:  lel2an 163  ler2an 165  ledi 166  ledio 168  ska4 415  i3orlem2 535  i3orlem3 536  ud4lem1a 559  test2 785  mlaoml 815  orbile 825  mlaconj4 826  mhlem 858  mh 861  mlaconjo 868  oago3.21x 872  gon2n 878  go2n4 879  go2n6 881  oa4lem3 919  oa3to4lem3 927  oa4to6lem4 943  oa4btoc 946  oa4uto4g 955  oa4uto4 957  oa3-6lem 960  mloa 998

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