If you want your logic to be [classical](https://en.wikipedia.org/wiki/Classical_logic) (i.e. to validate principles like the law of double negation), then as Emil Jeřábek says in comments, you can derive disjunction in terms of implication as $\varphi \lor \psi := (\varphi \to \psi) \to \psi$.  Generally, in classical logics, there are so many ways to interdefine the connectives that it’s hard to give a not-too-weak system that doesn’t imply the full usual system.

On the other hand, **if you are happy for your logic to end up constructive/intuitionistic** (i.e. not be able to prove the law of double negation, excluded middle, etc), **then yes, logics of this sort have been studied.**

The two I’m most familiar with that omit disjunction are [regular logic](http://ncatlab.org/nlab/show/regular+logic) and the fragment of Martin-Löf Type Theory valid in any LCCC (see [Martin Hofmann](http://www.tcs.ifi.lmu.de/mitarbeiter/martin-hofmann/my-publications), *On the interpretation of type theory in locally cartesian closed categories*), i.e. with just function types and product types.

However, both of these sound like overkill for your case — what you outline sounds more like the conjunction-implication fragment of [intuitionistic logic](https://en.wikipedia.org/wiki/Intuitionistic_logic).  The [sequent caluclus presentation](https://en.wikipedia.org/wiki/Sequent_calculus) nicely separates the rules for the various connectives, so that each one still works fine in the absence of the others.  I don’t know anywhere that this specific fragment has been studied/discussed, I’m afraid, though I would guess that it has been.