Theorem nsb

Any substitution in an always false formula is false. (Contributed by Steven Nguyen, 3-May-2023.)

Conclusion
\( \vdash \forall x \, \neg \varphi \rightarrow \neg [ t' / x ] \, \varphi \)
Proof
alnex
l1
biimpi _
\( \vdash \forall x \, \neg \varphi \rightarrow \neg \exists x \, \varphi \)
spsbe
\( \vdash [ t' / x ] \, \varphi \rightarrow \exists x \, \varphi \)
nsyl l1 _