Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3expa | Unicode version |
Description: Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.) |
Ref | Expression |
---|---|
3exp.1 |
Ref | Expression |
---|---|
3expa |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3exp.1 | . . 3 | |
2 | 1 | 3exp 1184 | . 2 |
3 | 2 | imp31 254 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 w3a 963 |
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 df-3an 965 |
This theorem is referenced by: ad4ant123 1197 ad4ant124 1198 ad4ant134 1199 ad4ant234 1200 3anidm23 1279 mp3an2 1307 mpd3an3 1320 rgen3 2544 moi2 2893 sbc3ie 3010 preq12bg 3736 issod 4279 wepo 4319 reuhypd 4431 funimass4 5519 fvtp1g 5675 f1imass 5724 fcof1o 5739 f1ofveu 5812 f1ocnvfv3 5813 acexmid 5823 2ndrn 6131 frecrdg 6355 oawordriexmid 6417 mapxpen 6793 findcard 6833 findcard2 6834 findcard2s 6835 ltapig 7258 ltanqi 7322 ltmnqi 7323 lt2addnq 7324 lt2mulnq 7325 prarloclemcalc 7422 genpassl 7444 genpassu 7445 prmuloc 7486 ltexprlemm 7520 ltexprlemfl 7529 ltexprlemfu 7531 lteupri 7537 ltaprg 7539 mul4 8007 add4 8036 cnegexlem2 8051 cnegexlem3 8052 2addsub 8089 addsubeq4 8090 muladd 8259 ltleadd 8321 reapmul1 8470 apreim 8478 receuap 8543 p1le 8720 lemul12b 8732 lbinf 8819 zdiv 9252 fzind 9279 fnn0ind 9280 uzss 9459 qmulcl 9546 qreccl 9551 xrlttr 9702 xaddass 9773 icc0r 9830 iooshf 9856 elfz5 9920 elfz0fzfz0 10025 fzind2 10138 ioo0 10159 ico0 10161 ioc0 10162 expnegap0 10427 expineg2 10428 mulexpzap 10459 expsubap 10467 expnbnd 10541 facndiv 10613 bccmpl 10628 bcval5 10637 bcpasc 10640 crim 10758 climshftlemg 11199 2sumeq2dv 11268 hash2iun 11376 2cprodeq2dv 11465 dvdsval3 11687 dvdsnegb 11703 muldvds1 11711 muldvds2 11712 dvdscmul 11713 dvdsmulc 11714 dvds2ln 11719 divalgb 11815 ndvdssub 11820 gcddiv 11902 rpexp1i 12028 phiprmpw 12096 hashgcdeq 12113 innei 12563 iscnp4 12618 cnpnei 12619 cnnei 12632 cnconst 12634 ismeti 12746 isxmet2d 12748 elbl2ps 12792 elbl2 12793 xblpnfps 12798 xblpnf 12799 xblm 12817 blininf 12824 blssexps 12829 blssex 12830 blsscls2 12893 metss 12894 metrest 12906 metcn 12914 divcnap 12955 cdivcncfap 12987 |
Copyright terms: Public domain | W3C validator |