Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > expd | Unicode version |
Description: Exportation deduction. (Contributed by NM, 20-Aug-1993.) |
Ref | Expression |
---|---|
exp3a.1 |
Ref | Expression |
---|---|
expd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exp3a.1 | . . . 4 | |
2 | 1 | com12 30 | . . 3 |
3 | 2 | ex 114 | . 2 |
4 | 3 | com3r 79 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 107 |
This theorem is referenced by: expdimp 257 pm3.3 259 syland 291 exp32 363 exp4c 366 exp4d 367 exp42 369 exp44 371 exp5c 374 impl 378 mpan2d 425 a2and 548 pm2.6dc 852 3impib 1190 exp5o 1215 biassdc 1384 exbir 1423 expcomd 1428 expdcom 1429 mopick 2091 ralrimivv 2545 mob2 2904 reuind 2929 difin 3357 reupick3 3405 suctr 4396 tfisi 4561 relop 4751 funcnvuni 5254 fnun 5291 mpteqb 5573 funfvima 5713 poxp 6194 nnmass 6449 supisoti 6969 axprecex 7815 ltnsym 7978 nn0lt2 9266 fzind 9300 fnn0ind 9301 btwnz 9304 lbzbi 9548 ledivge1le 9656 elfz0ubfz0 10054 elfzo0z 10113 fzofzim 10117 flqeqceilz 10247 leexp2r 10503 bernneq 10569 cau3lem 11050 climuni 11228 mulcn2 11247 dvdsabseq 11779 ndvdssub 11861 bezoutlemmain 11925 rplpwr 11954 algcvgblem 11975 euclemma 12072 basis2 12644 txcnp 12869 metcnp3 13109 bj-charfunr 13585 |
Copyright terms: Public domain | W3C validator |