Theorem nfand 1930

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 369	. 2 |- ( ( ps /\ ch ) <-> -. ( ps -> -. ch ) )
2		nfand.1	. . . 4 |- ( ph -> F/ x ps )
3		nfand.2	. . . . 5 |- ( ph -> F/ x ch )
4	3	nfnd 1907	. . . 4 |- ( ph -> F/ x -. ch )
5	2, 4	nfimd 1922	. . 3 |- ( ph -> F/ x ( ps -> -. ch ) )
6	5	nfnd 1907	. 2 |- ( ph -> F/ x -. ( ps -> -. ch ) )
7	1, 6	nfxfrd 1651	1 |- ( ph -> F/ x ( ps /\ ch ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 367   F/wnf 1621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-12 1859

This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618  df-nf 1622

This theorem is referenced by:  nf3and  1931  nfbid  1938  nfeld  2624  nfreud  3027  nfrmod  3028  nfrmo  3030  nfrab  3036  nfifd  3957  nfdisj  4422  dfid3  4785  nfriotad  6240  axrepndlem1  8958  axrepndlem2  8959  axunndlem1  8961  axunnd  8962  axregndlem2  8969  axinfndlem1  8972  axinfnd  8973  axacndlem4  8977  axacndlem5  8978  axacnd  8979  riotasv2d  35085