Theorem nfan1 2199

Description: A closed form of nfan 1898. (Contributed by Mario Carneiro, 3-Oct-2016.) df-nf 1783 changed. (Revised by Wolf Lammen, 18-Sep-2021.) (Proof shortened by Wolf Lammen, 7-Jul-2022.)

Hypotheses

Ref	Expression
nfim1.1	⊢ Ⅎ𝑥𝜑
nfim1.2	⊢ (𝜑 → Ⅎ𝑥𝜓)

Assertion

Ref	Expression
nfan1	⊢ Ⅎ𝑥(𝜑 ∧ 𝜓)

Proof of Theorem nfan1

Step	Hyp	Ref	Expression
1		df-an 396	. 2 ⊢ ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))
2		nfim1.1	. . . 4 ⊢ Ⅎ𝑥𝜑
3		nfim1.2	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜓)
4	3	nfnd 1857	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜓)
5	2, 4	nfim1 2198	. . 3 ⊢ Ⅎ𝑥(𝜑 → ¬ 𝜓)
6	5	nfn 1856	. 2 ⊢ Ⅎ𝑥 ¬ (𝜑 → ¬ 𝜓)
7	1, 6	nfxfr 1852	1 ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395  Ⅎwnf 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-12 2176

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1779  df-nf 1783

This theorem is referenced by:  sb4b  2479  ralcom2  3376  sbcralt  3871  sbcrext  3872  csbiebt  3927  riota5f  7417  axrepndlem1  10633  axrepndlem2  10634  axunnd  10637  axpowndlem2  10639  axpowndlem3  10640  axpowndlem4  10641  axregndlem2  10644  axinfndlem1  10646  axinfnd  10647  axacndlem4  10651  axacndlem5  10652  axacnd  10653  fproddivf  16024  nfan1c  35088  wl-sbcom2d-lem1  37561  wl-mo2df  37572  wl-eudf  37574  wl-mo3t  37578  wl-ax11-lem4  37590  wl-ax11-lem6  37592