Theorem le2an 169

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 153	. 2 (a ^ c) =< (b ^ c)
3		le2.2	. . 3 c =< d
4	3	lelan 167	. 2 (b ^ c) =< (b ^ d)
5	2, 4	letr 137	1 (a ^ c) =< (b ^ d)

Syntax hints:   =< wle 2   ^ wa 7

This theorem is referenced by:  lel2an 171  ler2an 173  ledi 174  ledio 176  ska4 433  i3orlem2 553  i3orlem3 554  ud4lem1a 577  test2 803  mlaoml 833  orbile 843  mlaconj4 844  mhlem 876  mh 879  mlaconjo 886  oago3.21x 890  e2ast2 894  gon2n 898  go2n4 899  go2n6 901  oa4lem3 939  oa3to4lem3 947  oa4to6lem4 963  oa4btoc 966  oa4uto4g 975  oa4uto4 977  oa3-6lem 980  mloa 1018

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