 Ignoring, for now, the metaphor of defining a connective (we will come back to it in  §7),  there is a formal point here. If, in constructing a derivation, one uses an introduction rule to get a formula with a certain main operator, and then applies the corresponding elimination rule with that formula as (major) premiss, one has made an avoidable “detour” in the argumentation. It is easy to see in many cases that the detour could have been avoided: to use \(\land\)-E in this way is just to obtain (a second copy of) a formula that was already there to be used as a premiss of the \(\land\)-I,. Similarly, using \(\rightarrow\)-E after \(\rightarrow\)-I could be obtained more directly: the minor premise is an occurrence of the same formula as the hypothesis of the \(\rightarrow\)-I subproof, so simply use the steps of the subproof as lines of the main proof.