Proof of Theorem dn1dc
Step | Hyp | Ref
| Expression |
1 | | pm2.45 728 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif)
![ph ph](_varphi.gif) ![) )](rp.gif) |
2 | | imnan 680 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif)
![ph ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
3 | 1, 2 | mpbi 144 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
4 | 3 | biorfi 736 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
5 | | orcom 718 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![ph ph](_varphi.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![)
)](rp.gif) |
6 | | ordir 807 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![ph ph](_varphi.gif)
![ch ch](_chi.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![ch ch](_chi.gif) ![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
7 | 4, 5, 6 | 3bitri 205 |
. 2
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![ch ch](_chi.gif) ![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
8 | | pm4.45 774 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![th th](_theta.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
9 | | simprrl 529 |
. . . . . . 7
![( (](lp.gif) DECID DECID DECID DECID ![th th](_theta.gif) ![) )](rp.gif) ![)
)](rp.gif)
DECID ![ch ch](_chi.gif) ![) )](rp.gif) |
10 | | dcor 920 |
. . . . . . . . 9
DECID DECID DECID ![( (](lp.gif)
![th th](_theta.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
11 | 10 | imp 123 |
. . . . . . . 8
![( (](lp.gif) DECID DECID ![th th](_theta.gif)
DECID ![( (](lp.gif) ![th th](_theta.gif) ![) )](rp.gif) ![) )](rp.gif) |
12 | 11 | ad2antll 483 |
. . . . . . 7
![( (](lp.gif) DECID DECID DECID DECID ![th th](_theta.gif) ![) )](rp.gif) ![)
)](rp.gif)
DECID ![( (](lp.gif) ![th th](_theta.gif) ![) )](rp.gif) ![) )](rp.gif) |
13 | | anordc 941 |
. . . . . . 7
DECID DECID ![( (](lp.gif) ![th th](_theta.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![th th](_theta.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![th th](_theta.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
14 | 9, 12, 13 | sylc 62 |
. . . . . 6
![( (](lp.gif) DECID DECID DECID DECID ![th th](_theta.gif) ![) )](rp.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![th th](_theta.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![th th](_theta.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
15 | 8, 14 | syl5bb 191 |
. . . . 5
![( (](lp.gif) DECID DECID DECID DECID ![th th](_theta.gif) ![) )](rp.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![th th](_theta.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
16 | 15 | orbi2d 780 |
. . . 4
![( (](lp.gif) DECID DECID DECID DECID ![th th](_theta.gif) ![) )](rp.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif)
![ch ch](_chi.gif) ![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![th th](_theta.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
17 | 16 | anbi2d 460 |
. . 3
![( (](lp.gif) DECID DECID DECID DECID ![th th](_theta.gif) ![) )](rp.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![ch
ch](_chi.gif) ![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![ch
ch](_chi.gif) ![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![th th](_theta.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
18 | | dcor 920 |
. . . . . . . 8
DECID DECID DECID ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
19 | | dcn 828 |
. . . . . . . 8
DECID ![( (](lp.gif) ![ps ps](_psi.gif)
DECID ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) |
20 | 18, 19 | syl6 33 |
. . . . . . 7
DECID DECID DECID ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
21 | 20 | imp 123 |
. . . . . 6
![( (](lp.gif) DECID DECID ![ps ps](_psi.gif) DECID ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) |
22 | 21 | adantrr 471 |
. . . . 5
![( (](lp.gif) DECID DECID DECID DECID ![th th](_theta.gif) ![) )](rp.gif) ![)
)](rp.gif)
DECID ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) |
23 | | dcor 920 |
. . . . 5
DECID ![( (](lp.gif) ![ps ps](_psi.gif) DECID DECID ![(
(](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
24 | 22, 9, 23 | sylc 62 |
. . . 4
![( (](lp.gif) DECID DECID DECID DECID ![th th](_theta.gif) ![) )](rp.gif) ![)
)](rp.gif)
DECID ![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![) )](rp.gif) |
25 | | dcn 828 |
. . . . . . . 8
DECID DECID ![ch ch](_chi.gif) ![) )](rp.gif) |
26 | 9, 25 | syl 14 |
. . . . . . 7
![( (](lp.gif) DECID DECID DECID DECID ![th th](_theta.gif) ![) )](rp.gif) ![)
)](rp.gif)
DECID ![ch ch](_chi.gif) ![) )](rp.gif) |
27 | | dcn 828 |
. . . . . . . 8
DECID ![( (](lp.gif) ![th th](_theta.gif) DECID ![( (](lp.gif)
![th th](_theta.gif) ![) )](rp.gif) ![)
)](rp.gif) |
28 | 12, 27 | syl 14 |
. . . . . . 7
![( (](lp.gif) DECID DECID DECID DECID ![th th](_theta.gif) ![) )](rp.gif) ![)
)](rp.gif)
DECID ![( (](lp.gif) ![th th](_theta.gif) ![) )](rp.gif) ![) )](rp.gif) |
29 | | dcor 920 |
. . . . . . 7
DECID DECID ![( (](lp.gif) ![th th](_theta.gif)
DECID ![( (](lp.gif) ![( (](lp.gif) ![th th](_theta.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
30 | 26, 28, 29 | sylc 62 |
. . . . . 6
![( (](lp.gif) DECID DECID DECID DECID ![th th](_theta.gif) ![) )](rp.gif) ![)
)](rp.gif)
DECID ![( (](lp.gif) ![( (](lp.gif) ![th th](_theta.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
31 | | dcn 828 |
. . . . . 6
DECID ![( (](lp.gif)
![( (](lp.gif) ![th th](_theta.gif) ![) )](rp.gif) DECID ![( (](lp.gif) ![( (](lp.gif) ![th th](_theta.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
32 | 30, 31 | syl 14 |
. . . . 5
![( (](lp.gif) DECID DECID DECID DECID ![th th](_theta.gif) ![) )](rp.gif) ![)
)](rp.gif)
DECID ![( (](lp.gif) ![( (](lp.gif) ![th th](_theta.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
33 | | dcor 920 |
. . . . . 6
DECID DECID ![( (](lp.gif) ![( (](lp.gif) ![th th](_theta.gif) ![) )](rp.gif)
DECID ![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![th th](_theta.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
34 | 33 | imp 123 |
. . . . 5
![( (](lp.gif) DECID DECID ![( (](lp.gif)
![( (](lp.gif) ![th th](_theta.gif) ![) )](rp.gif) ![) )](rp.gif) DECID ![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![th th](_theta.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
35 | 32, 34 | syldan 280 |
. . . 4
![( (](lp.gif) DECID DECID DECID DECID ![th th](_theta.gif) ![) )](rp.gif) ![)
)](rp.gif)
DECID ![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![th th](_theta.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
36 | | anordc 941 |
. . . 4
DECID ![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif)
![ch ch](_chi.gif) DECID ![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![th th](_theta.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif)
![ch ch](_chi.gif) ![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![th th](_theta.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif)
![ch ch](_chi.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![th th](_theta.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
37 | 24, 35, 36 | sylc 62 |
. . 3
![( (](lp.gif) DECID DECID DECID DECID ![th th](_theta.gif) ![) )](rp.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![ch
ch](_chi.gif) ![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![th th](_theta.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![ch ch](_chi.gif)
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![th th](_theta.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
38 | 17, 37 | bitrd 187 |
. 2
![( (](lp.gif) DECID DECID DECID DECID ![th th](_theta.gif) ![) )](rp.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![ch
ch](_chi.gif) ![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif)
![ch ch](_chi.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![th th](_theta.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
39 | 7, 38 | syl5rbb 192 |
1
![( (](lp.gif) DECID DECID DECID DECID ![th th](_theta.gif) ![) )](rp.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif)
![ch ch](_chi.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![th th](_theta.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![) )](rp.gif) |