Theorem nfan1 2201

Description: A closed form of nfan 1899. (Contributed by Mario Carneiro, 3-Oct-2016.) df-nf 1784 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 1858	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜓)
5	2, 4	nfim1 2200	. . 3 ⊢ Ⅎ𝑥(𝜑 → ¬ 𝜓)
6	5	nfn 1857	. 2 ⊢ Ⅎ𝑥 ¬ (𝜑 → ¬ 𝜓)
7	1, 6	nfxfr 1853	1 ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

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

This theorem is referenced by:  sb4b  2473  ralcom2  3348  sbcralt  3832  sbcrext  3833  csbiebt  3888  riota5f  7354  axrepndlem1  10521  axrepndlem2  10522  axunnd  10525  axpowndlem2  10527  axpowndlem3  10528  axpowndlem4  10529  axregndlem2  10532  axinfndlem1  10534  axinfnd  10535  axacndlem4  10539  axacndlem5  10540  axacnd  10541  fproddivf  15929  nfan1c  35056  wl-sbcom2d-lem1  37540  wl-mo2df  37551  wl-eudf  37553  wl-mo3t  37557  wl-ax11-lem4  37569  wl-ax11-lem6  37571