This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nsb

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

		Ref	Expression
	Assertion	nsb	$⊢ \forall x \neg φ \to \neg [t/ x] φ$

Step	Hyp	Ref	Expression
1		alnex	$⊢ \forall x \neg φ \leftrightarrow \neg \exists x φ$
2	1	biimpi	$⊢ \forall x \neg φ \to \neg \exists x φ$
3		spsbe	$⊢ [t/ x] φ \to \exists x φ$
4	2 3	nsyl	$⊢ \forall x \neg φ \to \neg [t/ x] φ$