Explanations for description logic (DL) entailments provide important support for the design and maintenance of large ontologies. The "justifications" usually employed for this purpose in ontology editors pinpoint the parts of the ontology responsible for a given entailment. Proofs for entailments make the intermediate reasoning steps explicit, and thus explain how a consequence can actually be derived. We present an interactive system for exploring description logic proofs, called Evonne, which not only visualizes proofs of consequences for ontologies written in expressive DLs, but also offers several proof generation procedures and various functions for condensing large proofs.