Theorem sbn1

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

	Ref	Expression
Assertion	sbn1	$$⊢\left[t/x\right]\neg \phi \to \neg \left[t/x\right]\phi$$

Proof

Step	Hyp	Ref	Expression
1		fal	$$⊢\neg \perp$$
2	1	nsb	$$⊢\neg \left[t/x\right]\perp$$
3		pm2.21	$$⊢\neg \phi \to \left(\phi \to \perp \right)$$
4	3	sb2imi	$$⊢\left[t/x\right]\neg \phi \to \left(\left[t/x\right]\phi \to \left[t/x\right]\perp \right)$$
5	2 4	mtoi	$$⊢\left[t/x\right]\neg \phi \to \neg \left[t/x\right]\phi$$