Source: A Concise Introduction to Logic (12 Ed, 2014) by Patrick Hurley
[p 415:] Since, however, the first eight of these rules are applicable only to whole lines in an argument, as long as the quantifier is attached to a line these rules of inference cannot be applied—at least not to the kind of arguments we are about to consider. To provide for their application, four additional rules are required to remove quantifiers at the beginning of a proof sequence and to introduce them, when needed, at the end of the sequence. These four rules are called universal instantiation, universal generalization, existential instantiation, and existential generalization.
[p 464:] One further restriction that affects all four of these rules of inference requires that the rules be applied only to whole lines in a proof.
This answer exposes a gap in my understanding: Why can the Eight Rules of Implication apply only to whole lines? Without the above restriction, the argument in the aforesaid post of mine appears to succeed more simply; the proof would start at 11; 3-10 above would never be needed.
complex logical form
, if the above is true, then instead of an Indirect Proof, why not use Conditional Proof instead? Then using 1A as the Assumption of the Conditional Proof, you can start the proof at 11; 3-10 above would never be needed.