Theorem nfand 1863

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 1841	. . . 4 |- ( ph -> F/ x -. ch )
5	2, 4	nfimd 1855	. . 3 |- ( ph -> F/ x ( ps -> -. ch ) )
6	5	nfnd 1841	. 2 |- ( ph -> F/ x -. ( ps -> -. ch ) )
7	1, 6	nfxfrd 1617	1 |- ( ph -> F/ x ( ps /\ ch ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-12 1794

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-nf 1591

This theorem is referenced by:  nf3and  1864  nfbid  1871  nfeld  2624  nfreud  2999  nfrmod  3000  nfrmo  3002  nfrab  3008  nfifd  3928  nfdisj  4385  dfid3  4748  nfriotad  6172  axrepndlem1  8870  axrepndlem2  8871  axunndlem1  8873  axunnd  8874  axregndlem2  8883  axinfndlem1  8886  axinfnd  8887  axacndlem4  8891  axacndlem5  8892  axacnd  8893  riotasv2d  32966