Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > exp41 | Structured version Visualization version Unicode version |
Description: An exportation inference. (Contributed by NM, 26-Apr-1994.) |
Ref | Expression |
---|---|
exp41.1 |
Ref | Expression |
---|---|
exp41 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exp41.1 | . . 3 | |
2 | 1 | ex 450 | . 2 |
3 | 2 | exp31 630 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 384 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 197 df-an 386 |
This theorem is referenced by: ad5ant2345 1317 tz7.49 7540 supxrun 12146 injresinj 12589 fi1uzind 13279 brfi1indALT 13282 fi1uzindOLD 13285 brfi1indALTOLD 13288 swrdswrdlem 13459 swrdswrd 13460 2cshwcshw 13571 cshwcsh2id 13574 prmgaplem6 15760 cusgrsize2inds 26349 usgr2pthlem 26659 usgr2pth 26660 wwlksnext 26788 elwwlks2 26861 rusgrnumwwlks 26869 clwlkclwwlklem2a4 26898 clwlkclwwlklem2 26901 umgrhashecclwwlk 26955 clwlksfclwwlk 26962 1to3vfriswmgr 27144 frgrnbnb 27157 branmfn 28964 relowlpssretop 33212 broucube 33443 eel0001 38945 eel0000 38946 eel1111 38947 eel00001 38948 eel00000 38949 eel11111 38950 climrec 39835 bgoldbtbndlem4 41696 bgoldbtbnd 41697 tgoldbach 41705 tgoldbachOLD 41712 2zlidl 41934 2zrngmmgm 41946 lincsumcl 42220 |
Copyright terms: Public domain | W3C validator |