Theorem nfan1 1865

Description: A closed form of nfan 1866. (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 1814	. . . 4 |- ( ph -> ( ps -> A. x ps ) )
3	2	imdistani 690	. . 3 |- ( ( ph /\ ps ) -> ( ph /\ A. x ps ) )
4		nfan1.1	. . . 4 |- F/ x ph
5	4	19.28 1862	. . 3 |- ( A. x ( ph /\ ps ) <-> ( ph /\ A. x ps ) )
6	3, 5	sylibr 212	. 2 |- ( ( ph /\ ps ) -> A. x ( ph /\ ps ) )
7	6	nfi 1597	1 |- F/ x ( ph /\ ps )

Syntax hints:   -> wi 4   /\ wa 369   A.wal 1368   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-12 1794

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

This theorem is referenced by:  nfan  1866  ralcom2  2991  sbcralt  3375  sbcrextOLD  3376  sbcrext  3377  csbiebt  3418  riota5f  6189  axrepndlem1  8870  axrepndlem2  8871  axunnd  8874  axpowndlem2  8876  axpowndlem2OLD  8877  axpowndlem3  8878  axpowndlem4  8880  axregndlem2  8883  axinfndlem1  8886  axinfnd  8887  axacndlem4  8891  axacndlem5  8892  axacnd  8893  wl-sbcom2d-lem1  28553  wl-mo2dnae  28563  wl-mo3t  28565  wl-ax11-lem4  28572  wl-ax11-lem6  28574