Description: Lemma for mdsymi . (Contributed by NM, 1-Jul-2004) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mdsymlem1.1 | |
|
mdsymlem1.2 | |
||
mdsymlem1.3 | |
||
Assertion | mdsymlem2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mdsymlem1.1 | |
|
2 | mdsymlem1.2 | |
|
3 | mdsymlem1.3 | |
|
4 | 2 | hatomici | |
5 | simplll | |
|
6 | atelch | |
|
7 | atelch | |
|
8 | chub1 | |
|
9 | 6 7 8 | syl2an | |
10 | 9 | adantlr | |
11 | 10 | adantlr | |
12 | 1 2 3 | mdsymlem1 | |
13 | 6 12 | sylanl1 | |
14 | 13 | adantr | |
15 | 11 14 | jca | |
16 | 15 | anim1i | |
17 | anass | |
|
18 | 16 17 | sylib | |
19 | 18 | anasss | |
20 | oveq1 | |
|
21 | 20 | sseq2d | |
22 | sseq1 | |
|
23 | 22 | anbi1d | |
24 | 21 23 | anbi12d | |
25 | 24 | rspcev | |
26 | 5 19 25 | syl2anc | |
27 | 26 | exp32 | |
28 | 27 | reximdvai | |
29 | 4 28 | syl5 | |