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 1103 | . 2 |
3 | 2 | imp32 244 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 97 w3a 885 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 df-3an 887 |
This theorem is referenced by: 3adant3r1 1113 3adant3r2 1114 3adant3r3 1115 3adant1l 1127 3adant1r 1128 mp3an1 1219 soinxp 4410 sotri 4720 fnfco 5065 mpt2eq3dva 5569 fovrnda 5644 ovelrn 5649 grprinvd 5696 nnmsucr 6067 ltpopr 6693 ltexprlemdisj 6704 recexprlemdisj 6728 mul4 7145 add4 7172 2addsub 7225 addsubeq4 7226 subadd4 7255 muladd 7381 ltleadd 7441 divmulap 7654 divap0 7663 div23ap 7670 div12ap 7673 divsubdirap 7684 divcanap5 7690 divmuleqap 7693 divcanap6 7695 divdiv32ap 7696 letrp1 7814 lemul12b 7827 lediv1 7835 cju 7913 nndivre 7949 nndivtr 7955 nn0addge1 8228 nn0addge2 8229 peano2uz2 8345 uzind 8349 uzind3 8351 fzind 8353 fnn0ind 8354 uzind4 8531 qre 8560 irrmul 8581 rpdivcl 8608 rerpdivcl 8613 iccshftr 8862 iccshftl 8864 iccdil 8866 icccntr 8868 fzaddel 8922 fzrev 8946 frec2uzf1od 9192 expdivap 9305 2shfti 9432 iisermulc2 9860 |
Copyright terms: Public domain | W3C validator |