I'm trying to show $\models\varphi\rightarrow\ \models\varphi[\psi/p]$ where $\psi$ and $\varphi$ are propositional formula and $p$ is a propositional variable.
(which relates to this post: Do we need to prove that replacing any of the variables of a tautology by a compound proposition or true/false gives a tautology?).
I was asked to make a separate post :). This is my attempted proof. Any comments welcome! Edit: Note that I am going about the proof in the way that was suggested by the linked post. The first part of the proof is proving the Alonzo Church Lemma mentioned in the linked post and the second part (the last paragraph) is using the lemma to prove the result.
Suppose that $p_1,p_2...p_n,\ p$ are the distinct propositional variables amongst which are all the propositional variables found in $\varphi$ and $\psi$. Let $v$ be a truth assignment function such that $v(p_i)=a_i$, $v(\psi)=b$, $v(p)=b$ and $v(\varphi[\psi/p])=c$. Then we claim $v(\varphi)=c$ and will prove this by induction on the complexity of $\varphi$
Suppose that $\varphi$ has zero connectives. Then $\varphi$ is a propositional variable, say $q$. If $p\equiv q$ then $\varphi[\psi/p]=ψ$. And if $v(\psi)=b$, $v(p)=b$ and $v(\varphi[\psi/p])=c$ then $b=c$ and so $v(\varphi)=v(q)=v(p)=b=c$. And if $p\not\equiv q$ then $\varphi[\psi/p]=φ$. And if $v(\psi)=b, v(p)=b$ and $v(\varphi[\psi/p])=c$ then $v(\varphi)=v(\varphi[\psi/p])=c$.
Now suppose that whenever $\varphi$ has $k$ or fewer connectives and $v$ is a truth function such that $v(p_i)=a_i$, $v(\psi)=b$, $v(p)=b$ and $v(\varphi[\psi/p])=c$ then $v(\varphi)=c$. Suppose $\varphi$ has $k+1$ connectives and $p_1,p_2...p_n,\ p$ are the distinct propositional variables amongst which are all the propositional variables found in $\varphi$ and $\psi$. Suppose $\varphi$ is of the form $\left(\theta\wedge\zeta\right)$ and suppose $v$ is a truth function such that $v(p_i)=a_i$, $v(\psi)=b$, $v(p)=b$ and $v(\varphi[\psi/p])=c$. Then $p_1,p_2...p_n,\ p$ are the distinct propositional variables amongst which are all the propositional variables found in $\theta$ and $\psi$ and in $\zeta$ and $\psi$. Let $v(\theta[\psi/p])=d$ and $v(\zeta[\psi/p])=e$. Then by our induction hypothesis, $v(\theta)=d$ and $v(\zeta)=e$. And $v(\varphi[\psi/p])=v((\theta\wedge ζ)[\psi/p])=v(\theta[\psi/p]\wedge ζ[ψ/p])=v(\theta[\psi/p])\wedge v(\zeta[\psi/p])=d\wedge e$. So $c= d\wedge e$. And $v(\varphi)=v(\theta\wedge\zeta)=v(\theta)\wedge v(\zeta)=\ d\wedge e=c$. We can show the same result if $\varphi$ is of the form $\left(\theta\vee\zeta\right),\left(\theta\rightarrow\zeta\right),\left(\theta\leftrightarrow\zeta\right)$ or $\lnot\theta$. Hence our proposition holds if $\varphi$ has $k+1$ connectives, and hence, by induction, is true for an arbitrary number of connectives (3).
Now suppose $\lnot(\models\varphi[\psi/p])$. Then, by definition, there is a truth assignment function, $v$, such that $v(\varphi[\psi/p])$ is false. Suppose $p$ is not present in $\psi$. Then $p$ is not present in $\varphi[\psi/p]$. Let $v'$ be a new truth assignment function defined by $v'(q)=\ v(q)$ for all $q\neq p$ and $v'(p)=v(\psi)$. Then $v'(\varphi[\psi/p])$ is false and by (3), $v'(\varphi)$ is false and so $\lnot(\models\varphi)$. Hence by the contra-positive, $\models\varphi\rightarrow\ \models\varphi[\psi/p]$ $(1)$. Now let $\psi\equiv r$ where $r$ is a propositional variable different than $p$. Then as $p$ is not present in $r$, by $(1)$ $\models\varphi\rightarrow\ \models\varphi[r/p]$ $(2)$. Now assume $p$ is present in $\psi$. Then replace all values of $p$ in $\psi$ with a variable not in $\psi$ or $\varphi$ (say $r$) to form $\psi[r/p]$. Then by $(1)$ as $p$ does not occur in $\psi[r/p]$, $\models\varphi\rightarrow\ \models\varphi[\psi[r/p]/p]$. And by $(2)$ as $p$ is different than $r$, $\models\varphi[\psi[r/p]/p]\rightarrow\models\varphi[\psi[r/p]/p][p/r]$. And $\varphi[\psi[r/p]/p][p/r]\equiv\varphi[\psi/p]$. Hence $\models\varphi\rightarrow\models\varphi[\psi/p]$ in this instance as well.