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	⊢ Ⅎ 𝑥 𝜑
	nfan.2	⊢ Ⅎ 𝑥 𝜓
Assertion	nfnan	⊢ Ⅎ 𝑥 ( 𝜑 ⊼ 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		nfan.1	⊢ Ⅎ 𝑥 𝜑
2		nfan.2	⊢ Ⅎ 𝑥 𝜓
3		df-nan	⊢ ( ( 𝜑 ⊼ 𝜓 ) ↔ ¬ ( 𝜑 ∧ 𝜓 ) )
4	1 2	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝜓 )
5	4	nfn	⊢ Ⅎ 𝑥 ¬ ( 𝜑 ∧ 𝜓 )
6	3 5	nfxfr	⊢ Ⅎ 𝑥 ( 𝜑 ⊼ 𝜓 )