Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > bitr4d | Unicode version |
Description: Deduction form of bitr4i 186. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
bitr4d.1 | |
bitr4d.2 |
Ref | Expression |
---|---|
bitr4d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bitr4d.1 | . 2 | |
2 | bitr4d.2 | . . 3 | |
3 | 2 | bicomd 140 | . 2 |
4 | 1, 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: 3bitr2d 215 3bitr2rd 216 3bitr4d 219 3bitr4rd 220 mpbirand 437 mpbiran2d 438 bianabs 600 imordc 882 3anibar 1149 xor2dc 1368 bilukdc 1374 reuhypd 4392 opelresi 4830 iota1 5102 funbrfv2b 5466 dffn5im 5467 fneqeql 5528 f1ompt 5571 dff13 5669 fliftcnv 5696 isotr 5717 isoini 5719 caovord3 5944 releldm2 6083 tpostpos 6161 nnsssuc 6398 nnaordi 6404 iserd 6455 ecdmn0m 6471 qliftel 6509 qliftfun 6511 qliftf 6514 ecopovsym 6525 mapen 6740 supisolem 6895 cnvti 6906 omp1eomlem 6979 ctssdc 6998 isomnimap 7009 ismkvmap 7028 recmulnqg 7199 nqtri3or 7204 ltmnqg 7209 mullocprlem 7378 addextpr 7429 gt0srpr 7556 ltsosr 7572 ltasrg 7578 map2psrprg 7613 xrlenlt 7829 letri3 7845 subadd 7965 ltsubadd2 8195 lesubadd2 8197 suble 8202 ltsub23 8204 ltaddpos2 8215 ltsubpos 8216 subge02 8240 ltaddsublt 8333 reapneg 8359 apsym 8368 apti 8384 leltap 8387 ap0gt0 8402 divmulap 8435 divmulap3 8437 rec11rap 8471 ltdiv1 8626 ltdivmul2 8636 ledivmul2 8638 ltrec 8641 suprleubex 8712 nnle1eq1 8744 avgle1 8960 avgle2 8961 nn0le0eq0 9005 znnnlt1 9102 zleltp1 9109 elz2 9122 uzm1 9356 uzin 9358 difrp 9480 xrletri3 9588 xgepnf 9599 xltnegi 9618 xltadd1 9659 xposdif 9665 xleaddadd 9670 elioo5 9716 elfz5 9798 fzdifsuc 9861 elfzm11 9871 uzsplit 9872 elfzonelfzo 10007 qtri3or 10020 qavgle 10036 flqbi 10063 flqbi2 10064 zmodid2 10125 q2submod 10158 sqap0 10359 lt2sq 10366 le2sq 10367 nn0opthlem1d 10466 bcval5 10509 zfz1isolemiso 10582 shftfib 10595 mulreap 10636 caucvgrelemcau 10752 caucvgre 10753 elicc4abs 10866 abs2difabs 10880 cau4 10888 maxclpr 10994 negfi 10999 lemininf 11005 mul0inf 11012 xrlemininf 11040 xrminltinf 11041 clim2 11052 climeq 11068 fisumss 11161 fsumabs 11234 isumshft 11259 absefib 11477 dvdsval3 11497 dvdslelemd 11541 dvdsabseq 11545 dvdsflip 11549 dvdsssfz1 11550 zeo3 11565 ndvdsadd 11628 dvdssq 11719 algcvgblem 11730 lcmdvds 11760 ncoprmgcdgt1b 11771 isprm3 11799 phiprmpw 11898 discld 12305 isneip 12315 restopnb 12350 restopn2 12352 restdis 12353 lmbr2 12383 cnptoprest 12408 cnptoprest2 12409 tx1cn 12438 tx2cn 12439 txcnmpt 12442 txrest 12445 elbl2ps 12561 elbl2 12562 blcomps 12565 blcom 12566 xblpnfps 12567 xblpnf 12568 blpnf 12569 xmeter 12605 bdxmet 12670 metrest 12675 xmetxp 12676 metcn 12683 cncffvrn 12738 |
Copyright terms: Public domain | W3C validator |