Theorem nfand 2008

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

Hypotheses

Ref	Expression
nfand.1	|- ( ph -> F/ x ps )
nfand.2	|- ( ph -> F/ x ch )

Assertion

Ref	Expression
nfand	|- ( ph -> F/ x ( ps /\ ch ) )

Proof of Theorem nfand

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

Syntax hints:   -. wn 3   -> wi 4   /\ wa 371   F/wnf 1667

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-12 1933

This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664  df-nf 1668

This theorem is referenced by:  nf3and  2009  nfbid  2016  nfeld  2600  nfreud  2963  nfrmod  2964  nfrmo  2966  nfrab  2972  nfifd  3909  nfdisj  4385  dfid3  4750  nfriotad  6260  axrepndlem1  9017  axrepndlem2  9018  axunndlem1  9020  axunnd  9021  axregndlem2  9028  axinfndlem1  9030  axinfnd  9031  axacndlem4  9035  axacndlem5  9036  axacnd  9037  riotasv2d  32529