A "Rigorous" proof for this seemingly obvious proposition.

Question

In mendelson logic textbook , there is this proposition,(I will replace some letters to make it easier to read)

"If $P$ is a tautology containing as statement letters $A_1,A_2,\ldots,A_n$ and $Q$ arises from $T$ by substituting statement forms $B_1,B_2,\ldots,B_n$ for $A_1,A_2,\ldots,A_n,$ respectively, then $Q$ is a tautology;that is, substituting in a tautology yields a tautology"

This proposition seems way too obvious too me. Then I wondered, is there a rigorous proof of this proposition. There was a proof in the textbook:

"Assume that $P$ is a tautology. For any assignment of truth values to the statement letters in $Q$, the forms $B_1,B_2,\ldots,B_n$ have truth values $x_1,x_2,\ldots,x_n$ (where each $x_i$ is $T$ or $F$). If we assign the values $x_1,x_2,...,x_n$ to $A_1,A_2,\ldots,A_n,$ respectively, then the resulting truth value of $P$ is the truth value of $Q$ for the given assignment of truth values.Since $P$ is a tautology, this truth value must be $T.$ Thus, $Q$ always takes the value $T$."

The proposition itself is perfectly understandable and it is a very useful proposition(Maybe even too obvious for me). But the proof seems to be not even slightly understandable to me for some reason. I didn't found any other proofs for this theorem anywhere. Is there a better proof for this theorem or I am missing something? (Maybe the proposition is so obvious that proving it is impossible?)

Edit:I just noticed that when I said "I will replace some letters to make it easier to read" then that means "this proposition will stay true nomatter if i replace some symbols". But the proposition itself is "this proposition will stay true no matter if i replace some symbols". So it is like a propositon inside itself.So in shorter words, I am applying this proposition without even proving it in the first place. This is by far the weirdest part about this proposition to me.

Answer 1

Long comment

Maybe, a more lengthy approach can help, considering the case of a single atom $p$.

Let $F$ a formula and let $p$ a propositional symbol occurring in $F$. This means that the formula is a truth-function $F(p)$: for every truth value assigned to $p$, the truth table corresponding to $F$ will outputs a truth value.

But $F$ is a tautology: thus for every assignments of truth values to atoms, the truth table will produce the value TRUE.

Consider now the formula $F' := F[A/p]$, where $A$ is a formula whatever. Irrespective of the "form" of $A$, every assignment will output either TRUE or FALSE as truth value for the formula.

Thus, when $A$ is evaluated to TRUE, we have to consider the lines in the original truth table for $F$ where $p$ is evaluated to TRUE. Due to the fact that $A$ is a tautology, in those lines the formula $F$ has value TRUE; thus also $F'$ will have TRUE in those lines.

But also when in the original truth table for $F$ the atom $p$ is evaluated to FALSE, the corresponding lines for formula $F$ have value TRUE; thus also $F'$ will have TRUE in those lines.

The argument can be iterated, taking into account that a formula is an expression of finite length and thus only a finite number of atoms occurs into it.