Theorem nfnan

Description: If x is not free in ph and ps , then it is not free in ( ph -/\ ps ) . (Contributed by Scott Fenton, 2-Jan-2018)

	Ref	Expression
Hypotheses	nfan.1	$$⊢Ⅎx\phi$$
	nfan.2	$$⊢Ⅎx\psi$$
Assertion	nfnan	$$⊢Ⅎx\left(\phi ⊼\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		nfan.1	$$⊢Ⅎx\phi$$
2		nfan.2	$$⊢Ⅎx\psi$$
3		df-nan	$$⊢\left(\phi ⊼\psi \right)\leftrightarrow \neg \left(\phi \wedge \psi \right)$$
4	1 2	nfan	$$⊢Ⅎx\left(\phi \wedge \psi \right)$$
5	4	nfn	$$⊢Ⅎx\neg \left(\phi \wedge \psi \right)$$
6	3 5	nfxfr	$$⊢Ⅎx\left(\phi ⊼\psi \right)$$