Proof of Theorem xordidc
Step | Hyp | Ref
| Expression |
1 | | dcbi 921 |
. . . . 5
DECID DECID DECID ![( (](lp.gif)
![ch ch](_chi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
2 | 1 | imp 123 |
. . . 4
![( (](lp.gif) DECID DECID ![ch ch](_chi.gif)
DECID ![( (](lp.gif)
![ch ch](_chi.gif) ![) )](rp.gif) ![)
)](rp.gif) |
3 | | annimdc 922 |
. . . . . 6
DECID DECID ![( (](lp.gif) ![ch ch](_chi.gif) ![( (](lp.gif) ![(
(](lp.gif)
![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif)
![ch ch](_chi.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
4 | 3 | imp 123 |
. . . . 5
![( (](lp.gif) DECID DECID ![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![ch ch](_chi.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif)
![ch ch](_chi.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
5 | | pm5.32 449 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![ch ch](_chi.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ps
ps](_psi.gif)
![( (](lp.gif) ![ch
ch](_chi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
6 | 5 | notbii 658 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif)
![( (](lp.gif) ![(
(](lp.gif)
![ps ps](_psi.gif) ![( (](lp.gif)
![ch ch](_chi.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
7 | 4, 6 | syl6bb 195 |
. . . 4
![( (](lp.gif) DECID DECID ![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![ch ch](_chi.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif)
![( (](lp.gif) ![ch
ch](_chi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
8 | 2, 7 | sylan2 284 |
. . 3
![( (](lp.gif) DECID DECID
DECID ![ch ch](_chi.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![ch ch](_chi.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif)
![( (](lp.gif) ![ch
ch](_chi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
9 | | xornbidc 1370 |
. . . . . 6
DECID DECID ![( (](lp.gif) ![( (](lp.gif) ![ch ch](_chi.gif)
![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
10 | 9 | imp 123 |
. . . . 5
![( (](lp.gif) DECID DECID ![ch ch](_chi.gif)
![( (](lp.gif) ![( (](lp.gif)
![ch ch](_chi.gif) ![( (](lp.gif)
![ch ch](_chi.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
11 | 10 | adantl 275 |
. . . 4
![( (](lp.gif) DECID DECID
DECID ![ch ch](_chi.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![ch ch](_chi.gif)
![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
12 | 11 | anbi2d 460 |
. . 3
![( (](lp.gif) DECID DECID
DECID ![ch ch](_chi.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![ch ch](_chi.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif)
![ch ch](_chi.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
13 | | dcan 919 |
. . . . . 6
DECID DECID DECID ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
14 | 13 | imp 123 |
. . . . 5
![( (](lp.gif) DECID DECID ![ps ps](_psi.gif) DECID ![(
(](lp.gif)
![ps ps](_psi.gif) ![) )](rp.gif) ![)
)](rp.gif) |
15 | 14 | adantrr 471 |
. . . 4
![( (](lp.gif) DECID DECID
DECID ![ch ch](_chi.gif) ![) )](rp.gif) DECID ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) |
16 | | dcan 919 |
. . . . . 6
DECID DECID DECID ![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
17 | 16 | imp 123 |
. . . . 5
![( (](lp.gif) DECID DECID ![ch ch](_chi.gif) DECID ![(
(](lp.gif)
![ch ch](_chi.gif) ![) )](rp.gif) ![)
)](rp.gif) |
18 | 17 | adantrl 470 |
. . . 4
![( (](lp.gif) DECID DECID
DECID ![ch ch](_chi.gif) ![) )](rp.gif) DECID ![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![) )](rp.gif) |
19 | | xornbidc 1370 |
. . . 4
DECID ![( (](lp.gif) ![ps
ps](_psi.gif) 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) ![ps ps](_psi.gif)
![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
20 | 15, 18, 19 | sylc 62 |
. . 3
![( (](lp.gif) DECID DECID
DECID ![ch ch](_chi.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ps
ps](_psi.gif) ![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif)
![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
21 | 8, 12, 20 | 3bitr4d 219 |
. 2
![( (](lp.gif) DECID DECID
DECID ![ch ch](_chi.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![ch ch](_chi.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ps
ps](_psi.gif) ![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
22 | 21 | exp32 363 |
1
DECID DECID DECID
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |