Theorem nfand

Description: If in a context x is not free in ps and ch , then it is not free in ( ps /\ ch ) . (Contributed by Mario Carneiro, 7-Oct-2016)

	Ref	Expression
Hypotheses	nfand.1	$$⊢\phi \to Ⅎx\psi$$
	nfand.2	$$⊢\phi \to Ⅎx\chi$$
Assertion	nfand	$$⊢\phi \to Ⅎx\left(\psi \wedge \chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		nfand.1	$$⊢\phi \to Ⅎx\psi$$
2		nfand.2	$$⊢\phi \to Ⅎx\chi$$
3		df-an	$$⊢\left(\psi \wedge \chi \right)\leftrightarrow \neg \left(\psi \to \neg \chi \right)$$
4	2	nfnd	$$⊢\phi \to Ⅎx\neg \chi$$
5	1 4	nfimd	$$⊢\phi \to Ⅎx\left(\psi \to \neg \chi \right)$$
6	5	nfnd	$$⊢\phi \to Ⅎx\neg \left(\psi \to \neg \chi \right)$$
7	3 6	nfxfrd	$$⊢\phi \to Ⅎx\left(\psi \wedge \chi \right)$$