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 362 exp4c 365 exp4d 366 exp42 368 exp44 370 exp5c 373 impl 377 mpan2d 424 a2and 532 pm2.6dc 832 3impib 1164 exp5o 1189 biassdc 1358 exbir 1397 expcomd 1402 expdcom 1403 mopick 2055 ralrimivv 2490 mob2 2837 reuind 2862 difin 3283 reupick3 3331 suctr 4313 tfisi 4471 relop 4659 funcnvuni 5162 fnun 5199 mpteqb 5479 funfvima 5617 poxp 6097 nnmass 6351 supisoti 6865 axprecex 7656 ltnsym 7818 nn0lt2 9100 fzind 9134 fnn0ind 9135 btwnz 9138 lbzbi 9376 ledivge1le 9481 elfz0ubfz0 9870 elfzo0z 9929 fzofzim 9933 flqeqceilz 10059 leexp2r 10315 bernneq 10380 cau3lem 10854 climuni 11030 mulcn2 11049 dvdsabseq 11472 ndvdssub 11554 bezoutlemmain 11613 rplpwr 11642 algcvgblem 11657 euclemma 11751 basis2 12142 txcnp 12367 metcnp3 12607 |
Copyright terms: Public domain | W3C validator |