Theorem nfan1 1874

Description: A closed form of nfan 1875. (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 1823	. . . 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 1871	. . 3 |- ( A. x ( ph /\ ps ) <-> ( ph /\ A. x ps ) )
6	3, 5	sylibr 212	. 2 |- ( ( ph /\ ps ) -> A. x ( ph /\ ps ) )
7	6	nfi 1606	1 |- F/ x ( ph /\ ps )

Syntax hints:   -> wi 4   /\ wa 369   A.wal 1377   F/wnf 1599

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-12 1803

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-nf 1600

This theorem is referenced by:  nfan  1875  ralcom2  3026  sbcralt  3412  sbcrextOLD  3413  sbcrext  3414  csbiebt  3455  riota5f  6271  axrepndlem1  8968  axrepndlem2  8969  axunnd  8972  axpowndlem2  8974  axpowndlem2OLD  8975  axpowndlem3  8976  axpowndlem4  8978  axregndlem2  8981  axinfndlem1  8984  axinfnd  8985  axacndlem4  8989  axacndlem5  8990  axacnd  8991  wl-sbcom2d-lem1  29862  wl-mo2dnae  29872  wl-mo3t  29874  wl-ax11-lem4  29881  wl-ax11-lem6  29883