Description: Lemma for strong state theorem. (Contributed by NM, 2-Nov-1999) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | strlem3.1 | |
|
strlem3.2 | |
||
strlem3.3 | |
||
strlem3.4 | |
||
Assertion | strlem4 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | strlem3.1 | |
|
2 | strlem3.2 | |
|
3 | strlem3.3 | |
|
4 | strlem3.4 | |
|
5 | 1 | strlem2 | |
6 | 3 5 | ax-mp | |
7 | eldifi | |
|
8 | pjid | |
|
9 | 3 8 | mpan | |
10 | 9 | fveq2d | |
11 | eqeq2 | |
|
12 | 10 11 | syl5ib | |
13 | 7 12 | mpan9 | |
14 | 2 13 | sylbi | |
15 | 14 | oveq1d | |
16 | sq1 | |
|
17 | 15 16 | eqtrdi | |
18 | 6 17 | eqtrid | |