Proof of Theorem bilukdc
Step | Hyp | Ref
| Expression |
1 | | bicom 139 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif)
![( (](lp.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
2 | 1 | bibi1i 227 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![ps ps](_psi.gif) ![ch ch](_chi.gif) ![( (](lp.gif) ![( (](lp.gif) ![ph ph](_varphi.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![) )](rp.gif) |
3 | | biassdc 1374 |
. . . . . 6
DECID DECID DECID
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif)
![ph ph](_varphi.gif)
![ch ch](_chi.gif) ![( (](lp.gif) ![( (](lp.gif)
![ch ch](_chi.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
4 | 3 | imp31 254 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) DECID
DECID ![ph ph](_varphi.gif) DECID
![ch ch](_chi.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ph ph](_varphi.gif) ![ch ch](_chi.gif)
![( (](lp.gif) ![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
5 | 2, 4 | syl5bb 191 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) DECID
DECID ![ph ph](_varphi.gif) DECID
![ch ch](_chi.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![ch ch](_chi.gif)
![( (](lp.gif) ![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
6 | 5 | ancom1s 559 |
. . 3
![( (](lp.gif) ![( (](lp.gif) DECID
DECID ![ps ps](_psi.gif) DECID
![ch ch](_chi.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![ch ch](_chi.gif)
![( (](lp.gif) ![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
7 | | dcbi 921 |
. . . . . 6
DECID DECID DECID ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
8 | 7 | imp 123 |
. . . . 5
![( (](lp.gif) DECID DECID ![ps ps](_psi.gif) DECID ![(
(](lp.gif)
![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) |
9 | 8 | adantr 274 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) DECID
DECID ![ps ps](_psi.gif) DECID
![ch ch](_chi.gif) DECID ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) |
10 | | simpr 109 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) DECID
DECID ![ps ps](_psi.gif) DECID
![ch ch](_chi.gif) DECID ![ch ch](_chi.gif) ![) )](rp.gif) |
11 | | dcbi 921 |
. . . . . 6
DECID DECID DECID ![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
12 | | dcbi 921 |
. . . . . 6
DECID DECID ![( (](lp.gif) ![ch ch](_chi.gif)
DECID ![( (](lp.gif)
![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
13 | 11, 12 | syl9 72 |
. . . . 5
DECID DECID DECID
DECID ![( (](lp.gif)
![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
14 | 13 | imp31 254 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) DECID
DECID ![ps ps](_psi.gif) DECID
![ch ch](_chi.gif) DECID ![( (](lp.gif) ![( (](lp.gif)
![ch ch](_chi.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
15 | | biassdc 1374 |
. . . 4
DECID ![( (](lp.gif) ![ps ps](_psi.gif)
DECID
DECID ![( (](lp.gif) ![( (](lp.gif)
![ch ch](_chi.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif)
![ps ps](_psi.gif) ![ch ch](_chi.gif) ![( (](lp.gif)
![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![ch ch](_chi.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
16 | 9, 10, 14, 15 | syl3c 63 |
. . 3
![( (](lp.gif) ![( (](lp.gif) DECID
DECID ![ps ps](_psi.gif) DECID
![ch ch](_chi.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif)
![ch ch](_chi.gif) ![( (](lp.gif) ![( (](lp.gif)
![ch ch](_chi.gif) ![) )](rp.gif) ![)
)](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![ch ch](_chi.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
17 | 6, 16 | mpbid 146 |
. 2
![( (](lp.gif) ![( (](lp.gif) DECID
DECID ![ps ps](_psi.gif) DECID
![ch ch](_chi.gif) ![( (](lp.gif) ![( (](lp.gif)
![ps ps](_psi.gif) ![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
18 | | simplr 520 |
. . 3
![( (](lp.gif) ![( (](lp.gif) DECID
DECID ![ps ps](_psi.gif) DECID
![ch ch](_chi.gif) DECID ![ps ps](_psi.gif) ![) )](rp.gif) |
19 | 11 | imp 123 |
. . . 4
![( (](lp.gif) DECID DECID ![ch ch](_chi.gif) DECID ![(
(](lp.gif)
![ch ch](_chi.gif) ![) )](rp.gif) ![) )](rp.gif) |
20 | 19 | adantlr 469 |
. . 3
![( (](lp.gif) ![( (](lp.gif) DECID
DECID ![ps ps](_psi.gif) DECID
![ch ch](_chi.gif) DECID ![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![) )](rp.gif) |
21 | | biassdc 1374 |
. . 3
DECID DECID DECID ![( (](lp.gif)
![ch ch](_chi.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![( (](lp.gif)
![ch ch](_chi.gif) ![) )](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
22 | 10, 18, 20, 21 | syl3c 63 |
. 2
![( (](lp.gif) ![( (](lp.gif) DECID
DECID ![ps ps](_psi.gif) DECID
![ch ch](_chi.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![( (](lp.gif)
![ch ch](_chi.gif) ![) )](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
23 | 17, 22 | bitr4d 190 |
1
![( (](lp.gif) ![( (](lp.gif) DECID
DECID ![ps ps](_psi.gif) DECID
![ch ch](_chi.gif) ![( (](lp.gif) ![( (](lp.gif)
![ps ps](_psi.gif) ![( (](lp.gif) ![( (](lp.gif)
![ps ps](_psi.gif) ![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |