[proofplan] The argument separates the genuine forcing construction from the metatheoretic consistency bookkeeping. The assumption that $T$ is strong enough to formalise forcing over countable transitive models is the background which makes the stated forcing-extension hypothesis a meaningful uniform hypothesis over models of $T$; after that hypothesis is granted, the proof uses exactly its semantic output. First assume the stronger external hypothesis that a countable transitive model $M\models T$ exists. The stated forcing hypothesis then supplies a forcing extension $M[G]$ satisfying $\mathrm{ZFC}+\varphi$, so $\mathrm{ZFC}+\varphi$ has a model. A direct soundness argument for formal first-order proofs converts the existence of this model into syntactic consistency. The final implication follows only after adding the course metatheorem which turns the assumed consistency background for $T$ into the existence of such a countable transitive model. [/proofplan] [step:Use the forcing hypothesis to build a model of $\mathrm{ZFC}+\varphi$] Assume, in the ambient metatheory, that there exists a countable transitive set $M$ such that $(M,\in)\models T$. The hypothesis that $T$ extends enough set theory to formalise forcing over countable transitive models is used to ensure that this application of the forcing template is legitimate for such models of $T$. By the explicit forcing hypothesis of the theorem, applied to this $M$, there exist a forcing poset $\mathbb{P}\in M$ and an $M$-generic filter $G\subseteq \mathbb{P}$ such that the forcing extension $M[G]$ is defined and satisfies \begin{align*} M[G]\models \mathrm{ZFC}+\varphi. \end{align*} Define the theory \begin{align*} S:=\mathrm{ZFC}\cup\{\varphi\}. \end{align*} The displayed satisfaction statement says exactly that the structure $(M[G],\in)$ is a model of every sentence in $S$. Hence $S$ has a model in the ambient metatheory. [guided] We begin with the stronger external assumption that a countable transitive model of $T$ exists. This is stronger than the bare syntactic assertion $\operatorname{Con}(T)$; ordinary first-order consistency by itself does not supply a countable transitive model. Let $M$ be a countable transitive set with $(M,\in)\models T$. The theorem's forcing hypothesis is already formulated to include the output of the forcing construction: for this particular $M$, there are a forcing poset $\mathbb{P}\in M$ and an $M$-generic filter $G\subseteq \mathbb{P}$ such that $M[G]$ is a well-defined forcing extension and \begin{align*} M[G]\models \mathrm{ZFC}+\varphi. \end{align*} Now set \begin{align*} S:=\mathrm{ZFC}\cup\{\varphi\}. \end{align*} Saying that $M[G]\models \mathrm{ZFC}+\varphi$ means that every axiom of $\mathrm{ZFC}$ is true in the structure $(M[G],\in)$ and that $\varphi$ is true in the same structure. Therefore $(M[G],\in)$ is a model of the whole theory $S$. Thus the forcing construction has produced the one semantic object needed for relative consistency: a model of $\mathrm{ZFC}+\varphi$. [/guided] [/step] [step:Convert the model into syntactic consistency] We now show that $S$ is syntactically consistent. Suppose, toward a contradiction, that $S$ were inconsistent. Then there would be a formal first-order proof from premises in $S$ of a contradiction, for instance of the sentence \begin{align*} \exists x\,(x\neq x). \end{align*} Every line in a formal first-order proof from premises in $S$ is true in every model of $S$: axioms of $S$ are true by the definition of model, logical axioms are valid in all first-order structures with equality, and each inference rule preserves truth in every structure. Induction on the length of the alleged proof therefore shows that every model of $S$ would satisfy its final sentence $\exists x\,(x\neq x)$. But $(M[G],\in)$ is a model of $S$, while no first-order structure satisfies $\exists x\,(x\neq x)$ because equality is reflexive in every first-order structure with equality. This contradiction proves \begin{align*} \operatorname{Con}(S). \end{align*} Since $S=\mathrm{ZFC}\cup\{\varphi\}$, this is precisely \begin{align*} \operatorname{Con}(\mathrm{ZFC}+\varphi). \end{align*} [/step] [step:Apply the external model-existence metatheorem when it is available] The preceding steps prove the metatheoretic implication \begin{align*} \exists M\,\bigl(M \text{ is countable and transitive and } (M,\in)\models T\bigr) \implies \operatorname{Con}(\mathrm{ZFC}+\varphi). \end{align*} If the course's ambient metatheory additionally supplies the implication \begin{align*} \operatorname{Con}(T) \implies \exists M\,\bigl(M \text{ is countable and transitive and } (M,\in)\models T\bigr), \end{align*} then composing these two metatheoretic implications yields \begin{align*} \operatorname{Con}(T)\implies \operatorname{Con}(\mathrm{ZFC}+\varphi). \end{align*} This last statement depends on the stated external model-existence convention; without that convention, the forcing argument proves the consistency conclusion from the existence of a countable transitive model of $T$, not from bare syntactic consistency of $T$ alone. [/step]