Theorem: Propositional Tautology is Tautology in Predicate Logic

Let $\LL_1$ be the language of predicate logic.
Let $\LL_0$ be the language of propositional logic.
Let the basic WFFs of $\LL_1$ be the vocabulary of $\LL_0$.
Let $\mathbf A$ be a $\mathrm{BI}$-tautology of $\LL_0$, by considering the basic subformulas of $\mathbf A$ as part of the vocabulary of $\LL_0$.
Then $\mathbf A$ is a $\mathrm{PL_A}$-tautology of $\LL_1$.

Proof:
We proceed by the Principle of Structural Induction on the bottom-up specification of $\LL_1$, applied to $\mathbf A$.
Define $\map {v_F} {\mathbf A} = F$ for all basic WFFs $\mathbf A$ as a boolean interpretation for $\LL_0$.
Consider the case $\mathbf A$ is formed by either $\paren{ \mathbf W ~ \PP_n }$ or $\paren{ \mathbf W ~ \forall\exists }$.
Then $\mathbf A$ is basic, and therefore:
:$\map {v_F} {\mathbf A} = F$
meaning that $\mathbf A$ is not a $\mathrm{BI}$-tautology.
Consider next the case $\mathbf A$ is formed by either $\paren{ \mathbf W ~ \neg }$ or $\paren{ \mathbf W ~ \lor, \land, \Rightarrow, \Leftrightarrow }$.
That is, $\mathbf A = \neg \mathbf B$ or $\mathbf A = \mathbf B \circ \mathbf B'$ for $\circ$ being one of $\lor, \land, \Rightarrow, \Leftrightarrow$.
Suppose $\mathbf A$ is not a $\mathrm{PL_A}$-tautology.
Then there are a structure $\AA$ and an assignment $\sigma$ such that:
:$\AA, \sigma \not\models \mathbf A$
Then define the boolean interpretation $v_{\AA, \sigma}$ on basic WFFs $\mathbf B$ by:
:$\map {v_{\AA, \sigma} } {\mathbf B} = T$ {{iff}} $\AA, \sigma \models \mathbf B$
which is to say:
:$\map {v_{\AA, \sigma} } {\mathbf B} = \map {\operatorname{val}_\AA} {\mathbf B} \sqbrk \sigma$
where $\map {\operatorname{val}_\AA} {\mathbf B} \sqbrk \sigma$ is the value of $\mathbf A$ in $\AA$ under $\sigma$.
Hence, by definition of boolean interpretation:
{{begin-eqn}}
{{eqn|l = \map {v_{\AA, \sigma} } {\neg \mathbf B}
     |r = T
}}
{{eqn|ll = \leadstoandfrom
     |l  = \map {v_{\AA, \sigma} } {\mathbf B}
     |r  = F
}}
{{eqn|ll = \leadstoandfrom
     |l  = \AA, \sigma
     |o  = \not\models
     |r  = \mathbf B
}}
{{eqn|ll = \leadstoandfrom
     |l  = \AA, \sigma
     |o  = \models
     |r  = \neg \mathbf B
}}
{{end-eqn}}
And similarly, for $\circ$ being one of $\lor, \land, \Rightarrow, \Leftrightarrow$:
{{begin-eqn}}
{{eqn|l = \map {v_{\AA, \sigma} } {\mathbf B \circ \mathbf B'}
     |r = T
}}
{{eqn|ll = \leadstoandfrom
     |l  = \map {f^\circ} {\map {v_{\AA, \sigma} } {\mathbf B}, \map {v_{\AA, \sigma} } {\mathbf B'} }
     |r  = T
     |c  = {{Defof|Boolean Interpretation}}
}}
{{eqn|ll = \leadstoandfrom
     |l  = \map {f^\circ} {\map {\operatorname{val}_\AA} {\mathbf B} \sqbrk \sigma, \map {\operatorname{val}_\AA} {\mathbf B'} \sqbrk \sigma }
     |r  = T
     |c  = Definition of $v_{\AA, \sigma}$
}}
{{eqn|ll = \leadstoandfrom
     |l  = \map {\operatorname{val}_\AA} {\mathbf B \circ \mathbf B'} \sqbrk \sigma
     |r  = T
     |c  = {{Defof|Value of Formula under Assignment}}
}}
{{eqn|ll = \leadstoandfrom
     |l  = \AA, \sigma
     |o  = \models
     |r  = \mathbf B \circ \mathbf B'
}}
{{end-eqn}}
Since by hypothesis $\AA, \sigma \not\models \mathbf A$, it follows that:
:$\map {v_{\AA, \sigma} } {\mathbf A} = F$
and $\mathbf A$ is not a $\mathrm{BI}$-tautology.
The induction case for $\paren{ \mathbf W ~ \neg }$ and $\paren{ \mathbf W ~ \lor, \land, \Rightarrow, \Leftrightarrow }$ follows by transposition.
Hence the result by the Principle of Structural Induction.
{{qed}}