Theorem nfand 1826

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 386	. 2 |- ( ( ps /\ ch ) <-> -. ( ps -> -. ch ) )
2		nfand.1	. . . 4 |- ( ph -> F/ x ps )
3		nfand.2	. . . . 5 |- ( ph -> F/ x ch )
4	3	nfnd 1785	. . . 4 |- ( ph -> F/ x -. ch )
5	2, 4	nfimd 1823	. . 3 |- ( ph -> F/ x ( ps -> -. ch ) )
6	5	nfnd 1785	. 2 |- ( ph -> F/ x -. ( ps -> -. ch ) )
7	1, 6	nfxfrd 1780	1 |- ( ph -> F/ x ( ps /\ ch ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 384   F/wnf 1708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1705  df-nf 1710

This theorem is referenced by:  nf3and  1827  nfan  1828  nfbid  1832  nfeld  2773  nfreud  3112  nfrmod  3113  nfrmo  3115  nfrab  3123  nfifd  4114  nfdisj  4632  dfid3  5025  nfriotad  6619  axrepndlem1  9414  axrepndlem2  9415  axunndlem1  9417  axunnd  9418  axregndlem2  9425  axinfndlem1  9427  axinfnd  9428  axacndlem4  9432  axacndlem5  9433  axacnd  9434  riotasv2d  34243