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	⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 )
	nfand.2	⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 )
Assertion	nfand	⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝜓 ∧ 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		nfand.1	⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 )
2		nfand.2	⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 )
3		df-an	⊢ ( ( 𝜓 ∧ 𝜒 ) ↔ ¬ ( 𝜓 → ¬ 𝜒 ) )
4	2	nfnd	⊢ ( 𝜑 → Ⅎ 𝑥 ¬ 𝜒 )
5	1 4	nfimd	⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝜓 → ¬ 𝜒 ) )
6	5	nfnd	⊢ ( 𝜑 → Ⅎ 𝑥 ¬ ( 𝜓 → ¬ 𝜒 ) )
7	3 6	nfxfrd	⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝜓 ∧ 𝜒 ) )