![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > bitr4d | Unicode version |
Description: Deduction form of bitr4i 187. (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 141 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | bitrd 188 |
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: 3bitr2d 216 3bitr2rd 217 3bitr4d 220 3bitr4rd 221 mpbirand 441 mpbiran2d 442 bianabs 611 imordc 897 3anibar 1165 xor2dc 1390 bilukdc 1396 reuhypd 4473 opelresi 4920 iota1 5194 funbrfv2b 5562 dffn5im 5563 fneqeql 5626 f1ompt 5669 dff13 5771 fliftcnv 5798 isotr 5819 isoini 5821 caovord3 6050 releldm2 6188 tpostpos 6267 nnsssuc 6505 nnaordi 6511 iserd 6563 ecdmn0m 6579 qliftel 6617 qliftfun 6619 qliftf 6622 ecopovsym 6633 mapen 6848 supisolem 7009 cnvti 7020 omp1eomlem 7095 ctssdc 7114 isomnimap 7137 ismkvmap 7154 iswomnimap 7166 netap 7255 2omotaplemap 7258 recmulnqg 7392 nqtri3or 7397 ltmnqg 7402 mullocprlem 7571 addextpr 7622 gt0srpr 7749 ltsosr 7765 ltasrg 7771 map2psrprg 7806 xrlenlt 8024 letri3 8040 subadd 8162 ltsubadd2 8392 lesubadd2 8394 suble 8399 ltsub23 8401 ltaddpos2 8412 ltsubpos 8413 subge02 8437 ltaddsublt 8530 reapneg 8556 apsym 8565 apti 8581 leltap 8584 ap0gt0 8599 divmulap 8634 divmulap3 8636 rec11rap 8670 ltdiv1 8827 ltdivmul2 8837 ledivmul2 8839 ltrec 8842 suprleubex 8913 nnle1eq1 8945 avgle1 9161 avgle2 9162 nn0le0eq0 9206 znnnlt1 9303 zleltp1 9310 elz2 9326 uzm1 9560 uzin 9562 difrp 9694 xrletri3 9806 xgepnf 9818 xltnegi 9837 xltadd1 9878 xposdif 9884 xleaddadd 9889 elioo5 9935 elfz5 10019 fzdifsuc 10083 elfzm11 10093 uzsplit 10094 elfzonelfzo 10232 qtri3or 10245 qavgle 10261 flqbi 10292 flqbi2 10293 zmodid2 10354 q2submod 10387 sqap0 10589 lt2sq 10596 le2sq 10597 nn0opthlem1d 10702 bcval5 10745 zfz1isolemiso 10821 shftfib 10834 mulreap 10875 caucvgrelemcau 10991 caucvgre 10992 elicc4abs 11105 abs2difabs 11119 cau4 11127 maxclpr 11233 negfi 11238 lemininf 11244 mul0inf 11251 xrlemininf 11281 xrminltinf 11282 clim2 11293 climeq 11309 fisumss 11402 fsumabs 11475 isumshft 11500 absefib 11780 dvdsval3 11800 dvdslelemd 11851 dvdsabseq 11855 dvdsflip 11859 dvdsssfz1 11860 zeo3 11875 ndvdsadd 11938 dvdssq 12034 algcvgblem 12051 lcmdvds 12081 ncoprmgcdgt1b 12092 isprm3 12120 phiprmpw 12224 prmdiv 12237 pc11 12332 pcz 12333 pockthlem 12356 1arith 12367 ercpbllemg 12754 grpinvcnv 12943 eqger 13088 ablsubadd 13120 dvdsr02 13279 opprunitd 13284 unitsubm 13293 issubrg3 13373 aprval 13377 discld 13721 isneip 13731 restopnb 13766 restopn2 13768 restdis 13769 lmbr2 13799 cnptoprest 13824 cnptoprest2 13825 tx1cn 13854 tx2cn 13855 txcnmpt 13858 txrest 13861 elbl2ps 13977 elbl2 13978 blcomps 13981 blcom 13982 xblpnfps 13983 xblpnf 13984 blpnf 13985 xmeter 14021 bdxmet 14086 metrest 14091 xmetxp 14092 metcn 14099 cncfcdm 14154 reefiso 14283 m1lgs 14537 2lgsoddprmlem2 14539 |
Copyright terms: Public domain | W3C validator |