Theorem nexdh

Description: Deduction for generalization rule for negated wff. (Contributed by NM, 2-Jan-2002)

	Ref	Expression
Hypotheses	nexdh.1	$$⊢\phi \to \forall x\phi$$
	nexdh.2	$$⊢\phi \to \neg \psi$$
Assertion	nexdh	$$⊢\phi \to \neg \exists x\psi$$

Proof

Step	Hyp	Ref	Expression
1		nexdh.1	$$⊢\phi \to \forall x\phi$$
2		nexdh.2	$$⊢\phi \to \neg \psi$$
3	1 2	alrimih	$$⊢\phi \to \forall x\neg \psi$$
4		alnex	$$⊢\forall x\neg \psi \leftrightarrow \neg \exists x\psi$$
5	3 4	sylib	$$⊢\phi \to \neg \exists x\psi$$