Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > impexp | Unicode version |
Description: Import-export theorem. Part of Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 24-Mar-2013.) |
Ref | Expression |
---|---|
impexp |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm3.3 259 | . 2 | |
2 | pm3.31 260 | . 2 | |
3 | 1, 2 | impbii 125 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: imp4a 347 exp4a 364 imdistan 442 pm5.3 472 pm4.87 552 nan 687 pm4.14dc 885 pm5.6dc 921 2sb6 1977 2sb6rf 1983 2exsb 2002 mor 2061 eu2 2063 moanim 2093 r2alf 2487 r3al 2514 r19.23t 2577 ceqsralt 2757 rspc2gv 2846 ralrab 2891 ralrab2 2895 euind 2917 reu2 2918 reu3 2920 rmo4 2923 rmo3f 2927 reuind 2935 rmo2ilem 3044 rmo3 3046 ralss 3213 rabss 3224 raldifb 3267 unissb 3826 elintrab 3843 ssintrab 3854 dftr5 4090 repizf2lem 4147 reusv3 4445 tfi 4566 raliunxp 4752 fununi 5266 dff13 5747 dfsmo2 6266 tfr1onlemaccex 6327 tfrcllemaccex 6340 qliftfun 6595 nnnninfeq2 7105 prime 9311 raluz 9537 raluz2 9538 ralrp 9632 facwordi 10674 modfsummod 11421 nnwosdc 11994 isprm2 12071 isprm4 12073 metcnp 13306 limcdifap 13425 bdcriota 13918 |
Copyright terms: Public domain | W3C validator |