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