![]() |
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 1145 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | imp32 254 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 929 |
This theorem is referenced by: 3adant3r1 1155 3adant3r2 1156 3adant3r3 1157 3adant1l 1173 3adant1r 1174 mp3an1 1267 soinxp 4537 sotri 4860 fnfco 5220 mpt2eq3dva 5751 fovrnda 5826 ovelrn 5831 grprinvd 5878 nnmsucr 6289 fidifsnid 6667 exmidpw 6704 undiffi 6715 fidcenumlemim 6741 ltpopr 7251 ltexprlemdisj 7262 recexprlemdisj 7286 mul4 7711 add4 7740 2addsub 7793 addsubeq4 7794 subadd4 7823 muladd 7959 ltleadd 8021 divmulap 8239 divap0 8248 div23ap 8255 div12ap 8258 divsubdirap 8272 divcanap5 8278 divmuleqap 8281 divcanap6 8283 divdiv32ap 8284 div2subap 8399 letrp1 8406 lemul12b 8419 lediv1 8427 cju 8519 nndivre 8556 nndivtr 8562 nn0addge1 8817 nn0addge2 8818 peano2uz2 8952 uzind 8956 uzind3 8958 fzind 8960 fnn0ind 8961 uzind4 9175 qre 9209 irrmul 9231 rpdivcl 9258 rerpdivcl 9263 iccshftr 9560 iccshftl 9562 iccdil 9564 icccntr 9566 fzaddel 9622 fzrev 9647 frec2uzf1od 9962 expdivap 10137 2shfti 10396 iooinsup 10836 isermulc2 10899 dvds2add 11273 dvds2sub 11274 dvdstr 11276 alzdvds 11298 divalg2 11369 lcmgcdlem 11502 lcmgcdeq 11508 isprm6 11569 tgclb 11933 topbas 11935 neissex 12033 cnpnei 12086 psmetxrge0 12134 psmetlecl 12136 xmetlecl 12169 xmettpos 12172 elbl3ps 12196 elbl3 12197 metss 12296 comet 12301 bdxmet 12303 bdmet 12304 bl2ioo 12332 cncffvrn 12351 divccncfap 12359 |
Copyright terms: Public domain | W3C validator |