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 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  1148  dp53lemc  1163  dp35leme  1171  dp35lemc  1173  dp41lemb  1181  xdp41  1196  xdp53  1198  xxdp41  1199  xxdp53  1201  xdp45lem  1202  xdp43lem  1203  xdp45  1204  xdp43  1205  3dp43  1206  oadp35lemc  1209