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 798 biassdc 1358 pm5.24dc 1361 anxordi 1363 sbequ12a 1731 drex1 1754 sbcomxyyz 1923 sb9v 1931 csbiebt 3009 prsspwg 3649 bnd2 4067 copsex2t 4137 copsex2g 4138 fnssresb 5205 fcnvres 5276 dmfco 5457 funimass5 5505 fmptco 5554 cbvfo 5654 cbvexfo 5655 isocnv 5680 isoini 5687 isoselem 5689 riota2df 5718 ovmpodxf 5864 caovcanrd 5902 fidcenumlemrks 6809 ordiso2 6888 ltpiord 7095 dfplpq2 7130 dfmpq2 7131 enqeceq 7135 enq0eceq 7213 enreceq 7512 ltpsrprg 7579 mappsrprg 7580 cnegexlem3 7907 subeq0 7956 negcon1 7982 subexsub 8102 subeqrev 8106 lesub 8171 ltsub13 8173 subge0 8205 div11ap 8427 divmuleqap 8444 ltmuldiv2 8597 lemuldiv2 8604 nn1suc 8703 addltmul 8914 elnnnn0 8978 znn0sub 9077 prime 9108 indstr 9344 qapne 9387 qlttri2 9389 fz1n 9779 fzrev3 9822 fzonlt0 9899 divfl0 10024 modqsubdir 10121 fzfig 10158 sqrt11 10766 sqrtsq2 10770 absdiflt 10819 absdifle 10820 nnabscl 10827 minclpr 10963 xrnegiso 10986 xrnegcon1d 10988 clim2 11007 climshft2 11030 sumrbdc 11102 sinbnd 11373 cosbnd 11374 dvdscmulr 11434 dvdsmulcr 11435 oddm1even 11484 qredeq 11689 cncongr2 11697 isprm3 11711 prmrp 11735 sqrt2irr 11752 crth 11811 eltg3 12137 eltop 12149 eltop2 12150 eltop3 12151 lmbrf 12295 cncnpi 12308 txcn 12355 hmeoimaf1o 12394 ismet2 12434 xmseq0 12548 |
Copyright terms: Public domain | W3C validator |