The basic logic of proofs extends the usual propositional language by expressions of the form "*s* is a proof of *A*", for any proposition *A*. In this paper we explore the extension of its intuitionistic fragment to a language including expressions of the form "*t* is a proof of *B*, dependent from *s*being a proof of *A*". We aim at laying down a ground comparison with equivalent constructions present in theories of dependent types, especially those similarly based on the Brouwer-Heyting-Kolmogorov semantics. We further translate this extended language to a natural deduction calculus which allows for a double interpretation of the construction on which a proof term may depend: as actually proven, or valid assumption, or as possibly proven, locally true assumption. We show meta-theoretical properties for this calculus and explain normalisation to a language with only unconditional proofs. We conclude by stating the characterization of our calculus with standard intutionistic logic of proofs