Theorem nfan1 1982

Description: A closed form of nfan 1983. (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 1925	. . . 4 |- ( ph -> ( ps -> A. x ps ) )
3	2	imdistani 694	. . 3 |- ( ( ph /\ ps ) -> ( ph /\ A. x ps ) )
4		nfan1.1	. . . 4 |- F/ x ph
5	4	19.28 1979	. . 3 |- ( A. x ( ph /\ ps ) <-> ( ph /\ A. x ps ) )
6	3, 5	sylibr 215	. 2 |- ( ( ph /\ ps ) -> A. x ( ph /\ ps ) )
7	6	nfi 1670	1 |- F/ x ( ph /\ ps )

Syntax hints:   -> wi 4   /\ wa 370   A.wal 1435   F/wnf 1663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-12 1904

This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-nf 1664

This theorem is referenced by:  nfan  1983  ralcom2  2991  sbcralt  3369  sbcrext  3370  csbiebt  3412  riota5f  6282  axrepndlem1  9006  axrepndlem2  9007  axunnd  9010  axpowndlem2  9012  axpowndlem3  9013  axpowndlem4  9014  axregndlem2  9017  axinfndlem1  9019  axinfnd  9020  axacndlem4  9024  axacndlem5  9025  axacnd  9026  fproddivf  14008  wl-sbcom2d-lem1  31637  wl-mo2df  31647  wl-eudf  31649  wl-mo3t  31653  wl-ax11-lem4  31666  wl-ax11-lem6  31668