![]() |
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 115 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | com3r 79 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 108 |
This theorem is referenced by: expdimp 259 pm3.3 261 syland 293 exp32 365 exp4c 368 exp4d 369 exp42 371 exp44 373 exp5c 376 impl 380 mpan2d 428 a2and 558 pm2.6dc 862 3impib 1201 exp5o 1226 biassdc 1395 exbir 1436 expcomd 1441 expdcom 1442 mopick 2104 ralrimivv 2558 mob2 2919 reuind 2944 difin 3374 reupick3 3422 suctr 4423 tfisi 4588 relop 4779 funcnvuni 5287 fnun 5324 mpteqb 5609 funfvima 5751 poxp 6236 nnmass 6491 supisoti 7012 axprecex 7882 ltnsym 8046 nn0lt2 9337 fzind 9371 fnn0ind 9372 btwnz 9375 lbzbi 9619 ledivge1le 9729 elfz0ubfz0 10128 elfzo0z 10187 fzofzim 10191 flqeqceilz 10321 leexp2r 10577 bernneq 10644 cau3lem 11126 climuni 11304 mulcn2 11323 dvdsabseq 11856 ndvdssub 11938 bezoutlemmain 12002 rplpwr 12031 algcvgblem 12052 euclemma 12149 insubm 12879 grpinveu 12918 srgmulgass 13183 basis2 13709 txcnp 13932 metcnp3 14172 bj-charfunr 14723 |
Copyright terms: Public domain | W3C validator |