Theorem sbn1

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

	Ref	Expression
Assertion	sbn1	⊢ ( [ 𝑡 / 𝑥 ] ¬ 𝜑 → ¬ [ 𝑡 / 𝑥 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		nsb	⊢ ( ∀ 𝑥 ¬ ⊥ → ¬ [ 𝑡 / 𝑥 ] ⊥ )
2		fal	⊢ ¬ ⊥
3	1 2	mpg	⊢ ¬ [ 𝑡 / 𝑥 ] ⊥
4		pm2.21	⊢ ( ¬ 𝜑 → ( 𝜑 → ⊥ ) )
5	4	sb2imi	⊢ ( [ 𝑡 / 𝑥 ] ¬ 𝜑 → ( [ 𝑡 / 𝑥 ] 𝜑 → [ 𝑡 / 𝑥 ] ⊥ ) )
6	3 5	mtoi	⊢ ( [ 𝑡 / 𝑥 ] ¬ 𝜑 → ¬ [ 𝑡 / 𝑥 ] 𝜑 )