![]() |
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: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia3 107 |
This theorem is referenced by: expdimp 256 pm3.3 258 syland 288 exp32 358 exp4c 361 exp4d 362 exp42 364 exp44 366 exp5c 369 impl 373 mpan2d 420 a2and 526 pm2.6dc 800 3impib 1144 exp5o 1169 biassdc 1338 exbir 1377 expcomd 1382 expdcom 1383 mopick 2033 ralrimivv 2466 mob2 2809 reuind 2834 difin 3252 reupick3 3300 suctr 4272 tfisi 4430 relop 4617 funcnvuni 5117 fnun 5154 mpteqb 5429 funfvima 5565 poxp 6035 nnmass 6288 supisoti 6785 axprecex 7512 ltnsym 7668 nn0lt2 8926 fzind 8960 fnn0ind 8961 btwnz 8964 lbzbi 9200 ledivge1le 9302 elfz0ubfz0 9685 elfzo0z 9744 fzofzim 9748 flqeqceilz 9874 leexp2r 10124 bernneq 10189 cau3lem 10662 climuni 10836 mulcn2 10855 dvdsabseq 11275 ndvdssub 11357 bezoutlemmain 11414 rplpwr 11443 algcvgblem 11458 euclemma 11552 basis2 11898 metcnp3 12293 |
Copyright terms: Public domain | W3C validator |