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	|- ( ph -> F/ x ps )
	nfand.2	|- ( ph -> F/ x ch )
Assertion	nfand	|- ( ph -> F/ x ( ps /\ ch ) )

Proof

Step	Hyp	Ref	Expression
1		nfand.1	|- ( ph -> F/ x ps )
2		nfand.2	|- ( ph -> F/ x ch )
3		df-an	|- ( ( ps /\ ch ) <-> -. ( ps -> -. ch ) )
4	2	nfnd	|- ( ph -> F/ x -. ch )
5	1 4	nfimd	|- ( ph -> F/ x ( ps -> -. ch ) )
6	5	nfnd	|- ( ph -> F/ x -. ( ps -> -. ch ) )
7	3 6	nfxfrd	|- ( ph -> F/ x ( ps /\ ch ) )