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 441 pm5.3 467 pm4.87 547 nan 682 pm4.14dc 876 pm5.6dc 912 2sb6 1964 2sb6rf 1970 2exsb 1989 mor 2048 eu2 2050 moanim 2080 r2alf 2474 r3al 2501 r19.23t 2564 ceqsralt 2739 rspc2gv 2828 ralrab 2873 ralrab2 2877 euind 2899 reu2 2900 reu3 2902 rmo4 2905 rmo3f 2909 reuind 2917 rmo2ilem 3026 rmo3 3028 ralss 3194 rabss 3205 raldifb 3247 unissb 3802 elintrab 3819 ssintrab 3830 dftr5 4065 repizf2lem 4122 reusv3 4420 tfi 4541 raliunxp 4727 fununi 5238 dff13 5718 dfsmo2 6234 tfr1onlemaccex 6295 tfrcllemaccex 6308 qliftfun 6562 nnnninfeq2 7072 prime 9263 raluz 9489 raluz2 9490 ralrp 9582 facwordi 10614 modfsummod 11355 isprm2 11993 isprm4 11995 metcnp 12912 limcdifap 13031 bdcriota 13458 |
Copyright terms: Public domain | W3C validator |