![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3expb | Unicode version |
Description: Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.) |
Ref | Expression |
---|---|
3exp.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
3expb |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3exp.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | 3exp 1204 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | imp32 257 |
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 982 |
This theorem is referenced by: 3adant3r1 1214 3adant3r2 1215 3adant3r3 1216 3adant1l 1232 3adant1r 1233 mp3an1 1335 soinxp 4717 sotri 5045 fnfco 5412 mpoeq3dva 5964 fovcdmda 6044 ovelrn 6049 fnmpoovd 6244 nnmsucr 6517 fidifsnid 6903 exmidpw 6940 undiffi 6957 fidcenumlemim 6985 ltpopr 7629 ltexprlemdisj 7640 recexprlemdisj 7664 mul4 8124 add4 8153 2addsub 8206 addsubeq4 8207 subadd4 8236 muladd 8376 ltleadd 8438 divmulap 8667 divap0 8676 div23ap 8683 div12ap 8686 divsubdirap 8700 divcanap5 8706 divmuleqap 8709 divcanap6 8711 divdiv32ap 8712 div2subap 8829 letrp1 8840 lemul12b 8853 lediv1 8861 cju 8953 nndivre 8990 nndivtr 8996 nn0addge1 9257 nn0addge2 9258 peano2uz2 9395 uzind 9399 uzind3 9401 fzind 9403 fnn0ind 9404 uzind4 9624 qre 9661 irrmul 9683 rpdivcl 9715 rerpdivcl 9720 iccshftr 10030 iccshftl 10032 iccdil 10034 icccntr 10036 fzaddel 10095 fzrev 10120 frec2uzf1od 10443 expdivap 10611 2shfti 10881 iooinsup 11326 isermulc2 11389 dvds2add 11873 dvds2sub 11874 dvdstr 11876 alzdvds 11901 divalg2 11972 lcmgcdlem 12120 lcmgcdeq 12126 isprm6 12190 pcqcl 12349 mgmplusf 12853 grpinva 12873 ismndd 12921 idmhm 12944 issubm2 12948 submid 12952 0mhm 12961 resmhm 12962 resmhm2 12963 resmhm2b 12964 mhmco 12965 mhmima 12966 grpinvcnv 13035 grpinvnzcl 13039 grpsubf 13046 imasgrp2 13075 qusgrp2 13078 mhmfmhm 13082 mulgnnsubcl 13099 mulgnn0z 13114 mulgnndir 13116 issubg4m 13157 isnsg3 13171 nsgid 13179 qusadd 13198 ghmmhm 13217 ghmmhmb 13218 idghm 13223 resghm 13224 ghmf1 13237 kerf1ghm 13238 qusghm 13246 ablnsg 13296 srgfcl 13352 srgmulgass 13368 srglmhm 13372 srgrmhm 13373 opprringbg 13455 mulgass3 13460 subrngringnsg 13577 issubrng2 13582 issubrg2 13613 islmodd 13634 lmodscaf 13651 lcomf 13668 rmodislmodlem 13691 issubrgd 13793 qusmul2 13868 crngridl 13869 qusmulrng 13871 psraddcl 13981 tgclb 14050 topbas 14052 neissex 14150 cnpnei 14204 txcnp 14256 psmetxrge0 14317 psmetlecl 14319 xmetlecl 14352 xmettpos 14355 elbl3ps 14379 elbl3 14380 metss 14479 comet 14484 bdxmet 14486 bdmet 14487 bl2ioo 14527 divcnap 14540 cncfcdm 14554 divccncfap 14562 dvrecap 14662 cosz12 14686 |
Copyright terms: Public domain | W3C validator |