Theorem nfan1 2030

Description: A closed form of nfan 2031. (Contributed by Mario Carneiro, 3-Oct-2016.)

Hypotheses

Ref	Expression
nfan1.1	|- F/ x ph
nfan1.2	|- ( ph -> F/ x ps )

Assertion

Ref	Expression
nfan1	|- F/ x ( ph /\ ps )

Proof of Theorem nfan1

Step	Hyp	Ref	Expression
1		nfan1.2	. . . . 5 |- ( ph -> F/ x ps )
2	1	nfrd 1973	. . . 4 |- ( ph -> ( ps -> A. x ps ) )
3	2	imdistani 704	. . 3 |- ( ( ph /\ ps ) -> ( ph /\ A. x ps ) )
4		nfan1.1	. . . 4 |- F/ x ph
5	4	19.28 2027	. . 3 |- ( A. x ( ph /\ ps ) <-> ( ph /\ A. x ps ) )
6	3, 5	sylibr 217	. 2 |- ( ( ph /\ ps ) -> A. x ( ph /\ ps ) )
7	6	nfi 1682	1 |- F/ x ( ph /\ ps )

Syntax hints:   -> wi 4   /\ wa 376   A.wal 1450   F/wnf 1675

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-12 1950

This theorem depends on definitions:  df-bi 190  df-an 378  df-ex 1672  df-nf 1676

This theorem is referenced by:  nfan  2031  ralcom2  2941  sbcralt  3328  sbcrext  3329  csbiebt  3369  riota5f  6294  axrepndlem1  9035  axrepndlem2  9036  axunnd  9039  axpowndlem2  9041  axpowndlem3  9042  axpowndlem4  9043  axregndlem2  9046  axinfndlem1  9048  axinfnd  9049  axacndlem4  9053  axacndlem5  9054  axacnd  9055  fproddivf  14118  wl-sbcom2d-lem1  31959  wl-mo2df  31969  wl-eudf  31971  wl-mo3t  31975  wl-ax11-lem4  31982  wl-ax11-lem6  31984