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		nsb	$$⊢\forall x\neg \perp \to \neg \left[t/x\right]\perp$$
2		fal	$$⊢\neg \perp$$
3	1 2	mpg	$$⊢\neg \left[t/x\right]\perp$$
4		pm2.21	$$⊢\neg \phi \to \left(\phi \to \perp \right)$$
5	4	sb2imi	$$⊢\left[t/x\right]\neg \phi \to \left(\left[t/x\right]\phi \to \left[t/x\right]\perp \right)$$
6	3 5	mtoi	$$⊢\left[t/x\right]\neg \phi \to \neg \left[t/x\right]\phi$$