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 27 | . . 3 |
3 | 2 | ex 108 | . 2 |
4 | 3 | com3r 73 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 97 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia3 101 |
This theorem is referenced by: expdimp 246 pm3.3 248 syland 277 exp32 347 exp4c 350 exp4d 351 exp42 353 exp44 355 exp5c 358 impl 362 mpan2d 404 pm2.6dc 759 3impib 1102 exp5o 1123 biassdc 1286 exbir 1325 expcomd 1330 expdcom 1331 mopick 1978 ralrimivv 2400 mob2 2721 reuind 2744 difin 3174 reupick3 3222 suctr 4158 tfisi 4310 relop 4486 funcnvuni 4968 fnun 5005 mpteqb 5261 funfvima 5390 poxp 5853 nnmass 6066 axprecex 6954 ltnsym 7104 nn0lt2 8322 fzind 8353 fnn0ind 8354 btwnz 8357 lbzbi 8551 ledivge1le 8652 elfz0ubfz0 8982 elfzo0z 9040 fzofzim 9044 flqeqceilz 9160 leexp2r 9308 bernneq 9369 cau3lem 9710 climuni 9814 mulcn2 9833 algcvgblem 9888 |
Copyright terms: Public domain | W3C validator |