Theorem nfan1 2068

Description: A closed form of nfan 1828. (Contributed by Mario Carneiro, 3-Oct-2016.) df-nf 1710 changed. (Revised by Wolf Lammen, 18-Sep-2021.)

Hypotheses

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

Assertion

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

Proof of Theorem nfan1

Step	Hyp	Ref	Expression
1		df-an 386	. 2 |- ( ( ph /\ ps ) <-> -. ( ph -> -. ps ) )
2		nfim1.1	. . . 4 |- F/ x ph
3		nfim1.2	. . . . 5 |- ( ph -> F/ x ps )
4		nfnt 1782	. . . . 5 |- ( F/ x ps -> F/ x -. ps )
5	3, 4	syl 17	. . . 4 |- ( ph -> F/ x -. ps )
6	2, 5	nfim1 2067	. . 3 |- F/ x ( ph -> -. ps )
7	6	nfn 1784	. 2 |- F/ x -. ( ph -> -. ps )
8	1, 7	nfxfr 1779	1 |- F/ x ( ph /\ ps )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 384   F/wnf 1708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1705  df-nf 1710

This theorem is referenced by:  ralcom2  3104  sbcralt  3510  sbcrext  3511  sbcrextOLD  3512  csbiebt  3553  riota5f  6636  axrepndlem1  9414  axrepndlem2  9415  axunnd  9418  axpowndlem2  9420  axpowndlem3  9421  axpowndlem4  9422  axregndlem2  9425  axinfndlem1  9427  axinfnd  9428  axacndlem4  9432  axacndlem5  9433  axacnd  9434  fproddivf  14718  wl-sbcom2d-lem1  33342  wl-mo2df  33352  wl-eudf  33354  wl-mo3t  33358  wl-ax11-lem4  33365  wl-ax11-lem6  33367