Can you introduce a tautology directly into a proof?

If so, is there a rule or law for this technique?

Tautological Consequence (TautCon) is the rule by which you can introduce a previously established tautology.   If it has been proven, or otherwise accepted, to be a tautology in the logic system being used, then you may use it.

In this case you are using Law of Excluded Middle, which is accepted in classical logic, but not in constructive logic.

---

EG: The Law of Excluded Middle is provable in a classical logic natural deduction system with the rule of Double Negation Elimination.$$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline #2\end{array}}\fitch{}{\fitch{\neg(\phi\vee\neg\phi)}{\fitch{\phi}{\phi\vee\neg\phi\quad\vee\mathsf I\\\bot\hspace{8ex}\neg\mathsf E}\\\neg\phi\hspace{10.5ex}\neg\mathsf I\\\phi\vee\neg\phi\hspace{6ex}\vee\mathsf I\\\bot\hspace{12ex}\neg\mathsf E}\\\neg\neg(\phi\vee\neg\phi)\hspace{5ex}\neg\mathsf I\\\phi\vee\neg\phi\hspace{10ex}\neg\neg\mathsf E}$$

I think your reasoning is a bit circular. In a proof tree of a propositional calculus, the only premises you are allowed to have are (a) your assumptions, and (b) premises that are 'cancelled' by use of an inference rule (see, eg, the exercise cited here). But this still allows you to do what you want to do (in a sense). A tautology, by definition, is a statement that can be derived from no premises: it is always true. The particular example you give isn't quite appropriate, because that's the law of the excluded middle, which is an inference rule of classical logic and not a tautology (especially because it is not true in intuitionistic logic). The tautology I'm thinking of is $p \rightarrow p$, which can be introduced into your proof by adding $p$ as a premise and using an implication-introduction to derive $p \rightarrow p$ and cancel the premise-$p$.

So, yes, you can introduce tautologies wherever you want, because they require no premises to prove. You seem to understand this with your line about "introducing it via the conditional proof", but I do not see a difference between proving it from nothing and inserting it without proof, except that the latter is less formal.

Perhaps you are also interested in a bit more practical, theorem prover-oriented side.

Let's assume we know $1 + 1 = 2$ and use that to prove $(1 + 1) + 1 = 2 + 1$. Clearly, we can just use the first equality to replace $(1 + 1)$ by $2$ yielding our goal.

This toy example looks as follows in the theorem prover Coq:

(* vvv Just some imports *)
From Coq Require Import ssreflect ssrfun ssrbool.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

(* Actually we don't assume 1 + 1 = 2, but in fact prove it *)
Theorem thm: 1 + 1 = 2.
Proof.
  (* albeit by a powerful command which can prove it on its own without human
     intervention *)
  by auto.
Qed.

Theorem thm': (1 + 1) + 1 = 2 + 1.
Proof.
  (* Here we deduce `1 + 1 = 2` in an ad-hoc manner by just referencing
     the previous thm *)
  have U: (1 + 1 = 2) by apply: thm.

  (* Then we rewrite as explained in the answer text above *)
  by rewrite U.
Qed.

Hence, yes, similar to how a mathematician can pull a theorem out of thin air to insert it in their script, we can do so in Coq.

Note that a theorem is nothing else than a tautology. So you have cascade of interdependent theorems with axioms at the very top. But axioms behave very much the same way as theorems in Coq, so can also by used in have commands.