Can you introduce a tautology directly into a proof? For the sake of simplicity, let us restrict the context of this question to classical propositional logic. When formally evaluating the validity of an argument, is it permitted to immediately introduce a proposition that is a tautology? For example, given the premises
$p \rightarrow q$
$\neg p \rightarrow s$
am I permitted to introduce a new premise such as 
$p \vee \neg p$ 
and immediately conclude 
$q \vee s$ 
via disjunction elimination/constructive dilemma? If so, is there a formal rule or law for such a technique? 
I understand that one can derive a statement such as $p \vee \neg p$ via the conditional proof. But again, my question is regarding whether we are permitted to bypass those steps altogether and simply introduce the premise $p \vee \neg p$ with the understanding that it is a tautology via negation law. After all, why should we be prohibited from immediately introducing a statement that is always true?
If we are not permitted to do so, why not? Is it simply a matter of convention, or is there some logical error associated with doing so?
This question has been in the back of mind ever since I started learning about logic. I've never seen the technique used and never understood why.
It may look something like this...


*

*$p \rightarrow q$ premise

*$\neg p \rightarrow s$ premise

*$T$ tautological introduction

*$p \vee \neg p$ negation law, 3

*$q \vee s$ disjunction elimination, 1,2,4
 A: 
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}$$
A: 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.
A: 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.
A: Whether you can add in a tautology or not would depend on the proof assistant/checker you are using and the inference rules that tool permits. If you are doing it manually it depends on what the audience watching or reading your proof will permit you to use.
Here is a proof of the example using a Fitch-style proof checker:

I could add the premise $P \lor \lnot P$, but since I already have an LEM (law of the excluded middle) inference rule, it does not save me any work and it adds to the set of premises. However, after the list of premises, I could not add this as a line in the proof because this particular tool has no inference rule permitting that.
Also, although this tool has a disjunction elimination rule, I would need two subproofs in additional to the line containing the disjunction to use the rule as justification. This would be similar to what I provided above to reference LEM.
The advantage of using such tools is they make sure one is always using a well-formed formula and one is following the inference rules exactly. If one does that one can get a confirmation that the proof is correct. The disadvantage is that one has to follow those syntax and inference rules exactly.

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/
