Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3impia | Unicode version |
Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.) |
Ref | Expression |
---|---|
3impia.1 |
Ref | Expression |
---|---|
3impia |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3impia.1 | . . 3 | |
2 | 1 | ex 114 | . 2 |
3 | 2 | 3imp 1182 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 w3a 967 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 969 |
This theorem is referenced by: mopick2 2096 3gencl 2755 mob2 2901 moi 2904 reupick3 3402 disjne 3457 disji2 3969 tz7.2 4326 funopg 5216 fvun1 5546 fvopab6 5576 isores3 5777 ovmpt4g 5955 ovmpos 5956 ov2gf 5957 ofrval 6054 poxp 6191 smoel 6259 tfr1onlemaccex 6307 tfrcllemaccex 6320 nnaass 6444 qsel 6569 xpdom3m 6791 phpm 6822 ctssdc 7069 mkvprop 7113 prarloclem3 7429 aptisr 7711 axpre-apti 7817 axapti 7960 addn0nid 8263 divvalap 8561 letrp1 8734 p1le 8735 zextle 9273 zextlt 9274 btwnnz 9276 gtndiv 9277 uzind2 9294 fzind 9297 iccleub 9858 uzsubsubfz 9972 elfz0fzfz0 10051 difelfznle 10060 elfzo0le 10110 fzonmapblen 10112 fzofzim 10113 fzosplitprm1 10159 rebtwn2zlemstep 10178 qbtwnxr 10183 icogelb 10191 expcl2lemap 10457 expclzaplem 10469 expnegzap 10479 leexp2r 10499 expnbnd 10567 bcval4 10654 bccmpl 10656 absexpzap 11008 divalgb 11847 ndvdssub 11852 dvdsgcd 11930 dfgcd2 11932 rplpwr 11945 lcmgcdlem 11988 coprmdvds1 12002 qredeq 12007 prmdvdsexpr 12061 nnnn0modprm0 12166 pcexp 12220 difsqpwdvds 12248 prmpwdvds 12264 nnmindc 12324 elrestr 12506 mopni 13029 sincosq1lem 13293 logbgcd1irr 13432 |
Copyright terms: Public domain | W3C validator |