Theorem le2an 169

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

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 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:  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  l42modlem2  1150  dp53lemc  1165  dp35leme  1173  dp35lemc  1175  dp41lemb  1183  xdp41  1198  xdp53  1200  xxdp41  1201  xxdp53  1203  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208  oadp35lemc  1211