The famous double negation translation establishes an embedding of classical into intuitionistic logic. Curiously, the reverse direction has not been covered in literature. Utilizing a normal form for intuitionistic logic, we establish a small model property for intuitionistic propositional logic. We use this property for a direct encoding of the Kripke semantics into classical propositional logic and quantified boolean formulas. Next, we transfer the developed techniques to the first-order case and provide an embedding of intuitionistic first-order logic into classical first-order logic. Our goal here is an encoding that facilitates the use of state-of-the-art provers for classical first-order logic for determining intuitionistic validity. In an experimental evaluation, we show that our approach can compete with state-of-the-art provers for certain classes of benchmarks, in particular when the intuitionistic content is low. We further note that our constructions support the transfer of counter-models to validity, which is a desired feature in model checking applications.