Hilbert Space Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HSE Home  >  Th. List  >  mdsymlem1 Unicode version

Theorem mdsymlem1 22813
 Description: Lemma for mdsymi 22821. (Contributed by NM, 1-Jul-2004.) (New usage is discouraged.)
Hypotheses
Ref Expression
mdsymlem1.1
mdsymlem1.2
mdsymlem1.3
Assertion
Ref Expression
mdsymlem1
Distinct variable groups:   ,   ,
Allowed substitution hint:   ()

Proof of Theorem mdsymlem1
StepHypRef Expression
1 mdsymlem1.1 . . . . . . 7
2 chub2 21917 . . . . . . 7
31, 2mpan2 655 . . . . . 6
4 mdsymlem1.3 . . . . . 6
53, 4syl6sseqr 3146 . . . . 5
6 mdsymlem1.2 . . . . . . . 8
71, 6chjcomi 21877 . . . . . . 7
87sseq2i 3124 . . . . . 6
98biimpi 188 . . . . 5
105, 9anim12i 551 . . . 4
11 ssin 3298 . . . 4
1210, 11sylib 190 . . 3
14 chjcl 21766 . . . . . . . . 9
151, 14mpan 654 . . . . . . . 8
164, 15syl5eqel 2337 . . . . . . 7
1716adantr 453 . . . . . 6
18 chub1 21916 . . . . . . . . . 10
191, 18mpan 654 . . . . . . . . 9
2019, 4syl6sseqr 3146 . . . . . . . 8
2120anim2i 555 . . . . . . 7
2221ancoms 441 . . . . . 6
23 dmdi 22712 . . . . . . . 8
246, 23mp3anl1 1276 . . . . . . 7
251, 24mpanl1 664 . . . . . 6
2617, 22, 25syl2anc 645 . . . . 5
2726adantlr 698 . . . 4
28 incom 3269 . . . . . . 7
2928oveq1i 5720 . . . . . 6
30 chincl 21908 . . . . . . . . 9
316, 30mpan 654 . . . . . . . 8
32 chlejb1 21921 . . . . . . . . 9
331, 32mpan2 655 . . . . . . . 8
3416, 31, 333syl 20 . . . . . . 7
3534biimpa 472 . . . . . 6
3629, 35syl5eq 2297 . . . . 5
3736adantr 453 . . . 4
3827, 37eqtr3d 2287 . . 3