There are several issues with what you've said. First, you've not stated the rules clearly/correctly. The first rule would be something like: "If by assuming $P$ we can show $Q$, then we've proven $P\Rightarrow Q$." Next, not all statements are of the form $P\Rightarrow Q$. You presumably also want some way of using all these things that you are assuming. In Hilbert-style systems, this is typically modus ponens which states that if we know $P\Rightarrow Q$ and we know $P$ then we can conclude $Q$.
For a typical Hilbert-style system for propositional logic, there is only one rule: modus ponens. The only way to conclude anything in such a system is either 1) for it to be an instance of an axiom, or 2) via modus ponens. There is no concept of "assuming" something in a Hilbert-style system, so none of the rules you mention are part of a Hilbert-style system. Hilbert-style systems are rather inhumane though (but they are very minimalistic which makes them nice for proving meta-theorems about the proof system).
A proof system that much more closely matches informal proofs is natural deduction. (Closely, related is the sequent calculus which has a lot of nice properties but whose rules are usually less intuitive though often easier to work with.) In natural deduction, each connective has its own rules, each split into two groups: introduction rules and elimination rules. Introduction rules show how to conclude a statement involving a connective, while elimination rules show how to make use of a statement involving a connective. Natural deduction also has a notion of proving something under assumptions: hypothetical proofs. Modus ponens is the elimination rule for $\Rightarrow$ (and is called simply $\Rightarrow$-elimination in natural deduction), and the first rule you mention is the introduction rule. In these more structural proof systems, each connective is defined by the rules independently of the other connectives. Often in natural deduction systems, $\neg P$ is defined as $P\Rightarrow\bot$ where $\bot$ is the nullary connective that stands for the always false formula. It is defined by the elimination rule that if under some assumptions we can prove $\bot$, then under those same assumptions we can prove anything. That is, the principle of explosion is the elimination rule for $\bot$. There is no introduction rule.
To support classical logic, we need to add an extra rule or an axiom. Unlike the other rules, this rule will involve multiple connectives which weakens some of the nice properties about natural deduction. (The sequent calculus doesn't have this issue which is one of its nice aspects.) A common choice is essentially your third rule which I'll restate as: if under some assumptions including $\neg Q$ (i.e. $Q\implies \bot$) we can derive $\bot$, then we can prove $Q$ under the same assumptions excluding $\neg Q$. Your second rule is then derivable from the rules for elimination and introduction rules for $\Rightarrow$, the elimination rule for $\bot$, and this last rule.
For classical propositional logic, you could reduce every formula to one involving only $\Rightarrow$ and $\neg$ or $\Rightarrow$ and $\bot$. So the four rules indicated above suffice to prove everything for this logic. For first-order logic, you'll need to add additional rules for the quantifiers. Even Hilbert-style systems usually take universal generalization (i.e. $\forall$-introduction) as an additional rule. Still, proving $P\lor Q$ by assuming $\neg P$ and showing $Q$ will often be a bit silly. In natural deduction, $\lor$ has two introduction rules, namely: if we can prove $P$ (under some assumptions), then we can prove $P\lor Q$ (under the same assumptions), and if we can prove $Q$, then we can prove $P\lor Q$. These rules are derivable from the four rules mentioned above if we define $P\lor Q$ as $(P\Rightarrow\bot)\Rightarrow Q$. We can derive the rules for all the other propositional connectives in terms of the four rules I mentioned given suitable definitions of those connectives in terms of $\Rightarrow$ and $\bot$. We can also, of course, derive a limitless set of additional rules to capture common patterns of reasoning such as the contrapositive rule. We can also make a different choice for what connectives and rules we want to take as primitive.
While I would say the first rule you mention ($\Rightarrow$-introduction) is intimately related to $\Rightarrow$, the other two are not particularly related to it. They are intimately related to classical logic, but both are not necessary and, given some other rule/axiom to incorporate classical logic, both could potentially be derivable. There is no reason to include both of the latter two rules as being somehow special, while excluding the infinite number of other derivable rules that conclude $P\Rightarrow Q$.