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 1197 | . 2 |
3 | 2 | imp31 254 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 w3a 973 |
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 975 |
This theorem is referenced by: ad4ant123 1210 ad4ant124 1211 ad4ant134 1212 ad4ant234 1213 3anidm23 1292 mp3an2 1320 mpd3an3 1333 rgen3 2557 moi2 2911 sbc3ie 3028 preq12bg 3760 issod 4304 wepo 4344 reuhypd 4456 funimass4 5547 fvtp1g 5704 f1imass 5753 fcof1o 5768 f1ofveu 5841 f1ocnvfv3 5842 acexmid 5852 2ndrn 6162 frecrdg 6387 oawordriexmid 6449 mapxpen 6826 findcard 6866 findcard2 6867 findcard2s 6868 ltapig 7300 ltanqi 7364 ltmnqi 7365 lt2addnq 7366 lt2mulnq 7367 prarloclemcalc 7464 genpassl 7486 genpassu 7487 prmuloc 7528 ltexprlemm 7562 ltexprlemfl 7571 ltexprlemfu 7573 lteupri 7579 ltaprg 7581 mul4 8051 add4 8080 cnegexlem2 8095 cnegexlem3 8096 2addsub 8133 addsubeq4 8134 muladd 8303 ltleadd 8365 reapmul1 8514 apreim 8522 receuap 8587 p1le 8765 lemul12b 8777 lbinf 8864 zdiv 9300 fzind 9327 fnn0ind 9328 uzss 9507 qmulcl 9596 qreccl 9601 xrlttr 9752 xaddass 9826 icc0r 9883 iooshf 9909 elfz5 9973 elfz0fzfz0 10082 fzind2 10195 ioo0 10216 ico0 10218 ioc0 10219 expnegap0 10484 expineg2 10485 mulexpzap 10516 expsubap 10524 expnbnd 10599 facndiv 10673 bccmpl 10688 bcval5 10697 bcpasc 10700 crim 10822 climshftlemg 11265 2sumeq2dv 11334 hash2iun 11442 2cprodeq2dv 11531 dvdsval3 11753 dvdsnegb 11770 muldvds1 11778 muldvds2 11779 dvdscmul 11780 dvdsmulc 11781 dvds2ln 11786 divalgb 11884 ndvdssub 11889 gcddiv 11974 rpexp1i 12108 phiprmpw 12176 hashgcdeq 12193 pythagtriplem1 12219 pockthg 12309 infpnlem1 12311 4sqlem3 12342 mndpfo 12674 innei 12957 iscnp4 13012 cnpnei 13013 cnnei 13026 cnconst 13028 ismeti 13140 isxmet2d 13142 elbl2ps 13186 elbl2 13187 xblpnfps 13192 xblpnf 13193 xblm 13211 blininf 13218 blssexps 13223 blssex 13224 blsscls2 13287 metss 13288 metrest 13300 metcn 13308 divcnap 13349 cdivcncfap 13381 lgslem4 13698 lgscllem 13702 lgsneg1 13720 lgsne0 13733 |
Copyright terms: Public domain | W3C validator |