Theorem sbn1

One direction of sbn, using fewer axioms. Compare 19.2. (Contributed by Steven Nguyen, 18-Aug-2023.)

Conclusion
\( \vdash [ t' / x ] \, (\neg \varphi) \rightarrow \neg [ t' / x ] \, \varphi \)
Proof
l0
nsb
\( \vdash \forall x \, \neg \bot \rightarrow \neg [ t' / x ] \, \bot \)
fal
\( \vdash \neg \bot \)
l2
mpg l0 _
\( \vdash \neg [ t' / x ] \, \bot \)
pm2.21
sb2imi _
\( \vdash [ t' / x ] \, (\neg \varphi) \rightarrow [ t' / x ] \, \varphi \rightarrow [ t' / x ] \, \bot \)
mtoi l2 _