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 346 exp4a 363 imdistan 440 pm5.3 466 pm4.87 531 nan 666 pm4.14dc 860 pm5.6dc 896 2sb6 1937 2sb6rf 1943 2exsb 1962 mor 2019 eu2 2021 moanim 2051 r2alf 2429 r3al 2454 r19.23t 2516 ceqsralt 2687 rspc2gv 2775 ralrab 2818 ralrab2 2822 euind 2844 reu2 2845 reu3 2847 rmo4 2850 rmo3f 2854 reuind 2862 rmo2ilem 2970 rmo3 2972 ralss 3133 rabss 3144 raldifb 3186 unissb 3736 elintrab 3753 ssintrab 3764 dftr5 3999 repizf2lem 4055 reusv3 4351 tfi 4466 raliunxp 4650 fununi 5161 dff13 5637 dfsmo2 6152 tfr1onlemaccex 6213 tfrcllemaccex 6226 qliftfun 6479 prime 9118 raluz 9341 raluz2 9342 ralrp 9431 facwordi 10454 modfsummod 11195 isprm2 11725 isprm4 11727 metcnp 12608 limcdifap 12727 bdcriota 13008 |
Copyright terms: Public domain | W3C validator |