Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3expia | Unicode version |
Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.) |
Ref | Expression |
---|---|
3exp.1 |
Ref | Expression |
---|---|
3expia |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3exp.1 | . . 3 | |
2 | 1 | 3exp 1103 | . 2 |
3 | 2 | imp 115 | 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: mp3an3 1221 3gencl 2588 moi 2724 sotricim 4060 elirr 4266 en2lp 4278 suc11g 4281 3optocl 4418 sefvex 5196 f1oresrab 5329 ovmpt2s 5624 ov2gf 5625 poxp 5853 brtposg 5869 dfsmo2 5902 smoiun 5916 tfrlemibxssdm 5941 nnsucsssuc 6071 nnaordi 6081 nnawordex 6101 xpdom3m 6308 ordiso 6358 ltbtwnnqq 6513 prarloclem4 6596 addlocpr 6634 1idprl 6688 1idpru 6689 ltexprlemrnd 6703 recexprlemrnd 6727 recexprlem1ssl 6731 recexprlem1ssu 6732 recexprlemss1l 6733 recexprlemss1u 6734 aptisr 6863 axpre-apti 6959 ltxrlt 7085 axapti 7090 lttri3 7098 reapti 7570 apreap 7578 msqge0 7607 mulge0 7610 recexap 7634 mulap0b 7636 lt2msq 7852 zaddcl 8285 zdiv 8328 zextlt 8332 prime 8337 uzind2 8350 fzind 8353 lbzbi 8551 xltneg 8749 iocssre 8822 icossre 8823 iccssre 8824 fzen 8907 qbtwnzlemshrink 9104 rebtwn2zlemshrink 9108 expival 9257 expclzaplem 9279 expnegzap 9289 expaddzap 9299 expmulzap 9301 shftuz 9418 cau3lem 9710 climuni 9814 bj-peano4 10080 |
Copyright terms: Public domain | W3C validator |