Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > bitr3d | Unicode version |
Description: Deduction form of bitr3i 185. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
bitr3d.1 | |
bitr3d.2 |
Ref | Expression |
---|---|
bitr3d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bitr3d.1 | . . 3 | |
2 | 1 | bicomd 140 | . 2 |
3 | bitr3d.2 | . 2 | |
4 | 2, 3 | bitrd 187 | 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 3bitr3d 217 3bitr3rd 218 pm5.16 818 biassdc 1384 pm5.24dc 1387 anxordi 1389 sbequ12a 1760 drex1 1785 sbcomxyyz 1959 sb9v 1965 csbiebt 3079 prsspwg 3726 bnd2 4146 copsex2t 4217 copsex2g 4218 fnssresb 5294 fcnvres 5365 dmfco 5548 funimass5 5596 fmptco 5645 cbvfo 5747 cbvexfo 5748 isocnv 5773 isoini 5780 isoselem 5782 riota2df 5812 ovmpodxf 5958 caovcanrd 5996 fidcenumlemrks 6909 ordiso2 6991 ltpiord 7251 dfplpq2 7286 dfmpq2 7287 enqeceq 7291 enq0eceq 7369 enreceq 7668 ltpsrprg 7735 mappsrprg 7736 cnegexlem3 8066 subeq0 8115 negcon1 8141 subexsub 8261 subeqrev 8265 lesub 8330 ltsub13 8332 subge0 8364 div11ap 8587 divmuleqap 8604 ltmuldiv2 8761 lemuldiv2 8768 nn1suc 8867 addltmul 9084 elnnnn0 9148 znn0sub 9247 prime 9281 indstr 9522 qapne 9568 qlttri2 9570 fz1n 9969 fzrev3 10012 fzonlt0 10092 divfl0 10221 modqsubdir 10318 fzfig 10355 sqrt11 10967 sqrtsq2 10971 absdiflt 11020 absdifle 11021 nnabscl 11028 minclpr 11164 xrnegiso 11189 xrnegcon1d 11191 clim2 11210 climshft2 11233 sumrbdc 11306 prodrbdclem2 11500 fprodssdc 11517 sinbnd 11679 cosbnd 11680 dvdscmulr 11746 dvdsmulcr 11747 oddm1even 11797 qredeq 12007 cncongr2 12015 isprm3 12029 prmrp 12056 sqrt2irr 12073 crth 12135 pcdvdsb 12230 ssnnctlemct 12322 eltg3 12604 eltop 12616 eltop2 12617 eltop3 12618 lmbrf 12762 cncnpi 12775 txcn 12822 hmeoimaf1o 12861 ismet2 12901 xmseq0 13015 |
Copyright terms: Public domain | W3C validator |