Theorem nsb

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

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

Proof

Step	Hyp	Ref	Expression
1		alnex	⊢ ( ∀ 𝑥 ¬ 𝜑 ↔ ¬ ∃ 𝑥 𝜑 )
2	1	biimpi	⊢ ( ∀ 𝑥 ¬ 𝜑 → ¬ ∃ 𝑥 𝜑 )
3		spsbe	⊢ ( [ 𝑡 / 𝑥 ] 𝜑 → ∃ 𝑥 𝜑 )
4	2 3	nsyl	⊢ ( ∀ 𝑥 ¬ 𝜑 → ¬ [ 𝑡 / 𝑥 ] 𝜑 )