![]() |
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 1202 |
. 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 980 |
This theorem is referenced by: 3adant3r1 1212 3adant3r2 1213 3adant3r3 1214 3adant1l 1230 3adant1r 1231 mp3an1 1324 soinxp 4692 sotri 5019 fnfco 5385 mpoeq3dva 5932 fovcdmda 6011 ovelrn 6016 fnmpoovd 6209 nnmsucr 6482 fidifsnid 6864 exmidpw 6901 undiffi 6917 fidcenumlemim 6944 ltpopr 7572 ltexprlemdisj 7583 recexprlemdisj 7607 mul4 8066 add4 8095 2addsub 8148 addsubeq4 8149 subadd4 8178 muladd 8318 ltleadd 8380 divmulap 8608 divap0 8617 div23ap 8624 div12ap 8627 divsubdirap 8641 divcanap5 8647 divmuleqap 8650 divcanap6 8652 divdiv32ap 8653 div2subap 8770 letrp1 8781 lemul12b 8794 lediv1 8802 cju 8894 nndivre 8931 nndivtr 8937 nn0addge1 9198 nn0addge2 9199 peano2uz2 9336 uzind 9340 uzind3 9342 fzind 9344 fnn0ind 9345 uzind4 9564 qre 9601 irrmul 9623 rpdivcl 9653 rerpdivcl 9658 iccshftr 9968 iccshftl 9970 iccdil 9972 icccntr 9974 fzaddel 10032 fzrev 10057 frec2uzf1od 10379 expdivap 10544 2shfti 10811 iooinsup 11256 isermulc2 11319 dvds2add 11803 dvds2sub 11804 dvdstr 11806 alzdvds 11830 divalg2 11901 lcmgcdlem 12047 lcmgcdeq 12053 isprm6 12117 pcqcl 12276 mgmplusf 12664 grprinvd 12684 ismndd 12717 idmhm 12737 issubm2 12741 submid 12745 0mhm 12750 mhmco 12751 mhmima 12752 grpinvcnv 12814 grpinvnzcl 12818 grpsubf 12825 mhmfmhm 12857 mulgnnsubcl 12871 mulgnn0z 12885 mulgnndir 12887 srgfcl 12969 srgmulgass 12985 srglmhm 12989 srgrmhm 12990 opprringbg 13062 mulgass3 13066 tgclb 13198 topbas 13200 neissex 13298 cnpnei 13352 txcnp 13404 psmetxrge0 13465 psmetlecl 13467 xmetlecl 13500 xmettpos 13503 elbl3ps 13527 elbl3 13528 metss 13627 comet 13632 bdxmet 13634 bdmet 13635 bl2ioo 13675 divcnap 13688 cncfcdm 13702 divccncfap 13710 dvrecap 13810 cosz12 13834 |
Copyright terms: Public domain | W3C validator |