Step | Hyp | Ref
| Expression |
1 | | enq0er 7397 |
. . . . . . . . . . . . . 14
~Q0 |
2 | 1 | a1i 9 |
. . . . . . . . . . . . 13
~Q0 ~Q0 ~Q0
~Q0 ~Q0
~Q0 ~Q0
~Q0
~Q0 |
3 | | nnnq0lem1 7408 |
. . . . . . . . . . . . . 14
~Q0 ~Q0 ~Q0
~Q0 ~Q0
~Q0 ~Q0
~Q0
|
4 | | mulcmpblnq0 7406 |
. . . . . . . . . . . . . . 15
~Q0 |
5 | 4 | imp 123 |
. . . . . . . . . . . . . 14
~Q0 |
6 | 3, 5 | syl 14 |
. . . . . . . . . . . . 13
~Q0 ~Q0 ~Q0
~Q0 ~Q0
~Q0 ~Q0
~Q0
~Q0 |
7 | 2, 6 | erthi 6559 |
. . . . . . . . . . . 12
~Q0 ~Q0 ~Q0
~Q0 ~Q0
~Q0 ~Q0
~Q0
~Q0
~Q0 |
8 | | simprlr 533 |
. . . . . . . . . . . 12
~Q0 ~Q0 ~Q0
~Q0 ~Q0
~Q0 ~Q0
~Q0 ~Q0 |
9 | | simprrr 535 |
. . . . . . . . . . . 12
~Q0 ~Q0 ~Q0
~Q0 ~Q0
~Q0 ~Q0
~Q0 ~Q0 |
10 | 7, 8, 9 | 3eqtr4d 2213 |
. . . . . . . . . . 11
~Q0 ~Q0 ~Q0
~Q0 ~Q0
~Q0 ~Q0
~Q0 |
11 | 10 | expr 373 |
. . . . . . . . . 10
~Q0 ~Q0 ~Q0
~Q0 ~Q0 ~Q0
~Q0
~Q0 |
12 | 11 | exlimdvv 1890 |
. . . . . . . . 9
~Q0 ~Q0 ~Q0
~Q0 ~Q0 ~Q0
~Q0 ~Q0 |
13 | 12 | exlimdvv 1890 |
. . . . . . . 8
~Q0 ~Q0 ~Q0
~Q0 ~Q0 ~Q0
~Q0 ~Q0 |
14 | 13 | ex 114 |
. . . . . . 7
~Q0 ~Q0 ~Q0
~Q0 ~Q0
~Q0 ~Q0
~Q0 |
15 | 14 | exlimdvv 1890 |
. . . . . 6
~Q0 ~Q0 ~Q0
~Q0 ~Q0
~Q0 ~Q0
~Q0 |
16 | 15 | exlimdvv 1890 |
. . . . 5
~Q0 ~Q0 ~Q0
~Q0 ~Q0
~Q0 ~Q0
~Q0 |
17 | 16 | impd 252 |
. . . 4
~Q0 ~Q0 ~Q0
~Q0 ~Q0
~Q0 ~Q0
~Q0
|
18 | 17 | alrimivv 1868 |
. . 3
~Q0 ~Q0 ~Q0
~Q0 ~Q0
~Q0 ~Q0
~Q0
|
19 | | opeq12 3767 |
. . . . . . . . . . 11
|
20 | 19 | eceq1d 6549 |
. . . . . . . . . 10
~Q0 ~Q0 |
21 | 20 | eqeq2d 2182 |
. . . . . . . . 9
~Q0 ~Q0 |
22 | 21 | anbi1d 462 |
. . . . . . . 8
~Q0
~Q0 ~Q0
~Q0 |
23 | | simpl 108 |
. . . . . . . . . . . 12
|
24 | 23 | oveq1d 5868 |
. . . . . . . . . . 11
|
25 | | simpr 109 |
. . . . . . . . . . . 12
|
26 | 25 | oveq1d 5868 |
. . . . . . . . . . 11
|
27 | 24, 26 | opeq12d 3773 |
. . . . . . . . . 10
|
28 | 27 | eceq1d 6549 |
. . . . . . . . 9
~Q0 ~Q0 |
29 | 28 | eqeq2d 2182 |
. . . . . . . 8
~Q0 ~Q0 |
30 | 22, 29 | anbi12d 470 |
. . . . . . 7
~Q0 ~Q0 ~Q0 ~Q0
~Q0 ~Q0 |
31 | | opeq12 3767 |
. . . . . . . . . . 11
|
32 | 31 | eceq1d 6549 |
. . . . . . . . . 10
~Q0 ~Q0 |
33 | 32 | eqeq2d 2182 |
. . . . . . . . 9
~Q0 ~Q0 |
34 | 33 | anbi2d 461 |
. . . . . . . 8
~Q0
~Q0 ~Q0
~Q0 |
35 | | simpl 108 |
. . . . . . . . . . . 12
|
36 | 35 | oveq2d 5869 |
. . . . . . . . . . 11
|
37 | | simpr 109 |
. . . . . . . . . . . 12
|
38 | 37 | oveq2d 5869 |
. . . . . . . . . . 11
|
39 | 36, 38 | opeq12d 3773 |
. . . . . . . . . 10
|
40 | 39 | eceq1d 6549 |
. . . . . . . . 9
~Q0 ~Q0 |
41 | 40 | eqeq2d 2182 |
. . . . . . . 8
~Q0 ~Q0 |
42 | 34, 41 | anbi12d 470 |
. . . . . . 7
~Q0 ~Q0 ~Q0 ~Q0
~Q0
~Q0 |
43 | 30, 42 | cbvex4v 1923 |
. . . . . 6
~Q0
~Q0 ~Q0 ~Q0
~Q0 ~Q0 |
44 | 43 | anbi2i 454 |
. . . . 5
~Q0
~Q0 ~Q0 ~Q0
~Q0 ~Q0
~Q0 ~Q0 ~Q0
~Q0 ~Q0
~Q0 |
45 | 44 | imbi1i 237 |
. . . 4
~Q0
~Q0 ~Q0 ~Q0
~Q0 ~Q0
~Q0
~Q0 ~Q0
~Q0 ~Q0
~Q0
|
46 | 45 | 2albii 1464 |
. . 3
~Q0
~Q0 ~Q0 ~Q0
~Q0 ~Q0
~Q0
~Q0 ~Q0
~Q0 ~Q0
~Q0
|
47 | 18, 46 | sylibr 133 |
. 2
~Q0 ~Q0 ~Q0
~Q0 ~Q0 ~Q0
~Q0 ~Q0
|
48 | | eqeq1 2177 |
. . . . 5
~Q0
~Q0 |
49 | 48 | anbi2d 461 |
. . . 4
~Q0
~Q0 ~Q0 ~Q0
~Q0 ~Q0 |
50 | 49 | 4exbidv 1863 |
. . 3
~Q0
~Q0 ~Q0 ~Q0
~Q0 ~Q0 |
51 | 50 | mo4 2080 |
. 2
~Q0
~Q0 ~Q0 ~Q0
~Q0 ~Q0 ~Q0
~Q0 ~Q0
|
52 | 47, 51 | sylibr 133 |
1
~Q0 ~Q0 ~Q0
~Q0 ~Q0 |