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 1137 | . 2 |
3 | 2 | imp 122 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 102 w3a 919 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 df-3an 921 |
This theorem is referenced by: mp3an3 1257 3gencl 2633 moi 2775 sotricim 4078 elirr 4284 en2lp 4297 suc11g 4300 3optocl 4436 sefvex 5216 f1oresrab 5350 ovmpt2s 5644 ov2gf 5645 poxp 5873 brtposg 5892 dfsmo2 5925 smoiun 5939 tfrlemibxssdm 5964 nnsucsssuc 6094 nnaordi 6104 nnawordex 6124 xpdom3m 6331 ordiso 6447 pr2ne 6461 ltbtwnnqq 6605 prarloclem4 6688 addlocpr 6726 1idprl 6780 1idpru 6781 ltexprlemrnd 6795 recexprlemrnd 6819 recexprlem1ssl 6823 recexprlem1ssu 6824 recexprlemss1l 6825 recexprlemss1u 6826 aptisr 6955 axpre-apti 7051 ltxrlt 7178 axapti 7183 lttri3 7191 reapti 7679 apreap 7687 msqge0 7716 mulge0 7719 recexap 7743 mulap0b 7745 lt2msq 7964 zaddcl 8391 zdiv 8435 zextlt 8439 prime 8446 uzind2 8459 fzind 8462 lbzbi 8701 xltneg 8903 iocssre 8976 icossre 8977 iccssre 8978 fzen 9062 qbtwnzlemshrink 9258 rebtwn2zlemshrink 9262 qbtwnxr 9266 ioo0 9268 ioom 9269 ico0 9270 ioc0 9271 expival 9478 expclzaplem 9500 expnegzap 9510 expaddzap 9520 expmulzap 9522 shftuz 9705 cau3lem 10000 climuni 10132 divalgb 10325 ndvdssub 10330 dvdsgcd 10401 lcmgcdlem 10459 qredeu 10479 isprm3 10500 prmdvdsexpr 10529 prmexpb 10530 bj-peano4 10750 |
Copyright terms: Public domain | W3C validator |