![]() |
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 1202 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | imp31 256 |
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 df-3an 980 |
This theorem is referenced by: ad4ant123 1215 ad4ant124 1216 ad4ant134 1217 ad4ant234 1218 3anidm23 1297 mp3an2 1325 mpd3an3 1338 rgen3 2564 moi2 2920 sbc3ie 3038 preq12bg 3775 issod 4321 wepo 4361 reuhypd 4473 funimass4 5569 fvtp1g 5727 f1imass 5778 fcof1o 5793 f1ofveu 5866 f1ocnvfv3 5867 acexmid 5877 2ndrn 6187 frecrdg 6412 oawordriexmid 6474 mapxpen 6851 findcard 6891 findcard2 6892 findcard2s 6893 ltapig 7340 ltanqi 7404 ltmnqi 7405 lt2addnq 7406 lt2mulnq 7407 prarloclemcalc 7504 genpassl 7526 genpassu 7527 prmuloc 7568 ltexprlemm 7602 ltexprlemfl 7611 ltexprlemfu 7613 lteupri 7619 ltaprg 7621 mul4 8092 add4 8121 cnegexlem2 8136 cnegexlem3 8137 2addsub 8174 addsubeq4 8175 muladd 8344 ltleadd 8406 reapmul1 8555 apreim 8563 receuap 8629 p1le 8809 lemul12b 8821 lbinf 8908 zdiv 9344 fzind 9371 fnn0ind 9372 uzss 9551 qmulcl 9640 qreccl 9645 xrlttr 9798 xaddass 9872 icc0r 9929 iooshf 9955 elfz5 10020 elfz0fzfz0 10129 fzind2 10242 ioo0 10263 ico0 10265 ioc0 10266 expnegap0 10531 expineg2 10532 mulexpzap 10563 expsubap 10571 expnbnd 10647 facndiv 10722 bccmpl 10737 bcval5 10746 bcpasc 10749 crim 10870 climshftlemg 11313 2sumeq2dv 11382 hash2iun 11490 2cprodeq2dv 11579 dvdsval3 11801 dvdsnegb 11818 muldvds1 11826 muldvds2 11827 dvdscmul 11828 dvdsmulc 11829 dvds2ln 11834 divalgb 11933 ndvdssub 11938 gcddiv 12023 rpexp1i 12157 phiprmpw 12225 hashgcdeq 12242 pythagtriplem1 12268 pockthg 12358 infpnlem1 12360 4sqlem3 12391 imasaddfnlemg 12741 mndpfo 12846 grplmulf1o 12951 grplactcnv 12979 mulgnn0subcl 13006 mulgsubcl 13007 mulgdir 13025 issubg2m 13059 issubgrpd2 13060 nmzsubg 13080 eqgen 13097 srglmhm 13187 srgrmhm 13188 oppr1g 13263 dvdsrcl2 13279 crngunit 13291 subrgugrp 13372 subsubrg 13377 islmod 13392 lmodvsdir 13413 lmodvsass 13414 lsssubg 13475 lss1d 13481 lidlsubg 13578 lidlsubcl 13579 innei 13824 iscnp4 13879 cnpnei 13880 cnnei 13893 cnconst 13895 ismeti 14007 isxmet2d 14009 elbl2ps 14053 elbl2 14054 xblpnfps 14059 xblpnf 14060 xblm 14078 blininf 14085 blssexps 14090 blssex 14091 blsscls2 14154 metss 14155 metrest 14167 metcn 14175 divcnap 14216 cdivcncfap 14248 lgslem4 14565 lgscllem 14569 lgsneg1 14587 lgsne0 14600 |
Copyright terms: Public domain | W3C validator |