How/where is this technique generalised and proven for other (standard, first order) logical operations (if possible)? A method of natural deduction. Logic is something I am entirely self-taught in. Due to my resulting ignorance, it is difficult for me to search for the right things. Therefore, please excuse me if this has been asked before.
The Details:
In this YouTube video by Attic Philosophy, an approach to doing natural deduction proofs is demonstrated but neither proven nor rigorously defined. (It is just an introduction.)

Essentially, one works backwards. The example given is a proof of
$$p\to (q\to r)\vdash (s\to p)\to(q\to(s\to r)).$$
We start by assuming $p\to (q\to r)$, leaving a big gap, then writing $(s\to p)\to(q\to(s\to r))$, like so:
$$\begin{array}{|lc}
p\to (q\to r) & \\
\hline
 & \\
 & \\
 & \\
 & \\
 & \\
 & \\
 & \\
(s\to p)\to (q\to (s\to r)). &
\end{array}$$
Then we assume the first bit of the conclusion and do the same thing as above, like so:
$$\begin{array}{|lc}
p\to (q\to r) & \\
\hline
 \rlap{\begin{array}{|lc} s\to p & \\
\hline
 & \\
 & \\
 & \\
 & \\
 & \\
q\to (s\to r) & 
\end{array}}&\\
(s\to p)\to (q\to (s\to r)). &
\end{array}$$
And again:
$$\begin{array}{|lc}
p\to (q\to r) & \\
\hline
 \rlap{\begin{array}{|lc} s\to p & \\
\hline
\rlap{\begin{array}{|lc}
q & \\
\hline
 & \\
 & \\
 & \\
s\to r & \\
 \end{array}}& \\
q\to (s\to r) & 
\end{array}}&\\
(s\to p)\to (q\to (s\to r)). &
\end{array}$$
Once more:
$$\begin{array}{|lc}
p\to (q\to r) & \\
\hline
 \rlap{\begin{array}{|lc} s\to p & \\
\hline
\rlap{\begin{array}{|lc}
q & \\
\hline
\rlap{\begin{array}{|lc}
s & \\
\hline
 & \\
 & \\
r
 \end{array}}& \\
s\to r & \\
 \end{array}}& \\
q\to (s\to r) & 
\end{array}}&\\
(s\to p)\to (q\to (s\to r)). &
\end{array}$$
Now we fill in the gap using all the assumptions we like from above it, like so: because there's an $r$ in the first row, we can use modus ponens using $s$ and $s\to p$, which gives $p$, then again with $p$ and $p\to(q\to r)$ to get $q\to r$, from which we get $r$; this looks like:
$$\begin{array}{|lc}
p\to (q\to r) & \\
\hline
 \rlap{\begin{array}{|lc} s\to p & \\
\hline
\rlap{\begin{array}{|lc}
q & \\
\hline
\rlap{\begin{array}{|lc}
s & \\
\hline
p & \\
q\to r & \\
r
 \end{array}}& \\
s\to r & \\
 \end{array}}& \\
q\to (s\to r) & 
\end{array}}&\\
(s\to p)\to (q\to (s\to r)). &
\end{array}$$
The Question:

How/where is this technique generalised and proven for other (standard, first order) logical operations (if possible)?

Context:
I am familiar with the method of analytic tableaux.
To get an idea of my capabilities, see this question of mine:
An alternative, formal proof that $(\lnot\forall xPx)\to(\exists y(\lnot Py)).$
 A: Your strategy of proving a conditional by assuming the antecedent and trying to get to the consequent (i.e. doping a conditional proof) is an excellent strategy.  And there are other strategies:

*

*If you want to prove $\neg \phi$, try to do a proof by contradiction: assume $\phi$, and see if you can get to a contradiction


*If you want to prove $\phi \land \psi$, try and prove $\phi$ and $\psi$ individually


*If you want to prove $\phi \lor \psi$, try one of the following 3 methods:



*

*Maybe there is a fairly easy way to get to $\phi$ or $\psi$ by themselves (unlikely to happen if this is the overall goal of a human-constructed logic problem, but often occurs within a subproof)


*See if among the statements that you have you have some other disjunction, e.g. $\chi \lor \lambda$, and set up a proof by cases on that one (oftentimes, one of $\chi$ or $\lambda$ will lead to $\phi$, and the other to $\psi$)


*Try a proof by contradiction: Assuming $\neg (\phi \lor \psi)$, you can go through a set pattern get both $\neg \phi$ and $\neg \psi$ and you may be well on your way to the contradiction you want.
Etc.
In fact, I could lay out a set of rules that, when followed in a certain order as an algorithm, systematically crank out formal proofs for any valid argument, whether in propositional logic or full first-order logic.
However, in order for such an algorithm to be guaranteed to always find a proof there is a cost: the proof it comes up with isn't always the most efficient .. sometimes far from it!
Simple example. Suppose I have two premises, $P$ and $P \to (Q \to (R \to (S \to T)))$, and my goal is $Q \to (R \to (S \to T))$. Strictly following the strategy of proving any conditional using conditional proofs, you'd create a bunch of nested subproofs, but it's obvious that in this case that is not needed at all.
So, in practice, a 'master' of formal proofs will see all of these strategies as heuristics: something that often works nicely, but that isn't always the fastest or most elegant. And it is experience that will tell them what will work well in what situation.
