![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > bitr2d | Unicode version |
Description: Deduction form of bitr2i 185. (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 188 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | bicomd 141 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: 3bitrrd 215 3bitr2rd 217 pm5.18dc 884 drex1 1809 elrnmpt1 4896 xpopth 6202 sbcopeq1a 6213 ltnnnq 7453 ltaddsub 8424 leaddsub 8426 posdif 8443 lesub1 8444 ltsub1 8446 lesub0 8467 possumd 8557 subap0 8631 ltdivmul 8864 ledivmul 8865 zlem1lt 9340 zltlem1 9341 negelrp 9719 fzrev2 10117 fz1sbc 10128 elfzp1b 10129 qtri3or 10275 sumsqeq0 10633 sqrtle 11080 sqrtlt 11081 absgt0ap 11143 iser3shft 11389 dvdssubr 11881 gcdn0gt0 12014 divgcdcoprmex 12137 pcfac 12385 lmbrf 14192 logge0b 14788 loggt0b 14789 logle1b 14790 loglt1b 14791 lgsne0 14917 lgsprme0 14921 |
Copyright terms: Public domain | W3C validator |