Theorem nfand 1925

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

Hypotheses

Ref	Expression
nfand.1
nfand.2

Assertion

Ref	Expression
nfand

Proof of Theorem nfand

Step	Hyp	Ref	Expression
1		df-an 371	. 2
2		nfand.1	. . . 4
3		nfand.2	. . . . 5
4	3	nfnd 1902	. . . 4
5	2, 4	nfimd 1917	. . 3
6	5	nfnd 1902	. 2
7	1, 6	nfxfrd 1646	1

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

This theorem is referenced by:  nf3and  1926  nfbid  1933  nfeld  2627  nfreud  3030  nfrmod  3031  nfrmo  3033  nfrab  3039  nfifd  3969  nfdisj  4434  dfid3  4801  nfriotad  6265  axrepndlem1  8988  axrepndlem2  8989  axunndlem1  8991  axunnd  8992  axregndlem2  9001  axinfndlem1  9004  axinfnd  9005  axacndlem4  9009  axacndlem5  9010  axacnd  9011  riotasv2d  34688

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-12 1854

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-nf 1617