Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > bitr2d | Unicode version |
Description: Deduction form of bitr2i 184. (Contributed by NM, 9-Jun-2004.) |
Ref | Expression |
---|---|
bitr2d.1 | |
bitr2d.2 |
Ref | Expression |
---|---|
bitr2d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bitr2d.1 | . . 3 | |
2 | bitr2d.2 | . . 3 | |
3 | 1, 2 | bitrd 187 | . 2 |
4 | 3 | bicomd 140 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: 3bitrrd 214 3bitr2rd 216 pm5.18dc 853 drex1 1754 elrnmpt1 4760 xpopth 6042 sbcopeq1a 6053 ltnnnq 7199 ltaddsub 8166 leaddsub 8168 posdif 8185 lesub1 8186 ltsub1 8188 lesub0 8209 possumd 8298 subap0 8372 ltdivmul 8598 ledivmul 8599 zlem1lt 9068 zltlem1 9069 negelrp 9430 fzrev2 9820 fz1sbc 9831 elfzp1b 9832 qtri3or 9975 sumsqeq0 10326 sqrtle 10763 sqrtlt 10764 absgt0ap 10826 iser3shft 11070 dvdssubr 11451 gcdn0gt0 11578 divgcdcoprmex 11695 lmbrf 12295 |
Copyright terms: Public domain | W3C validator |