Theorem nfand 1872

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 371	. 2 |- ( ( ps /\ ch ) <-> -. ( ps -> -. ch ) )
2		nfand.1	. . . 4 |- ( ph -> F/ x ps )
3		nfand.2	. . . . 5 |- ( ph -> F/ x ch )
4	3	nfnd 1850	. . . 4 |- ( ph -> F/ x -. ch )
5	2, 4	nfimd 1864	. . 3 |- ( ph -> F/ x ( ps -> -. ch ) )
6	5	nfnd 1850	. 2 |- ( ph -> F/ x -. ( ps -> -. ch ) )
7	1, 6	nfxfrd 1626	1 |- ( ph -> F/ x ( ps /\ ch ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 369   F/wnf 1599

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-12 1803

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-nf 1600

This theorem is referenced by:  nf3and  1873  nfbid  1880  nfeld  2637  nfreud  3039  nfrmod  3040  nfrmo  3042  nfrab  3048  nfifd  3973  nfdisj  4435  dfid3  4802  nfriotad  6264  axrepndlem1  8979  axrepndlem2  8980  axunndlem1  8982  axunnd  8983  axregndlem2  8992  axinfndlem1  8995  axinfnd  8996  axacndlem4  9000  axacndlem5  9001  axacnd  9002  riotasv2d  34116