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  2480  ralcom2  3361  sbcralt  3852  sbcrext  3853  csbiebt  3908  riota5f  7395  axrepndlem1  10611  axrepndlem2  10612  axunnd  10615  axpowndlem2  10617  axpowndlem3  10618  axpowndlem4  10619  axregndlem2  10622  axinfndlem1  10624  axinfnd  10625  axacndlem4  10629  axacndlem5  10630  axacnd  10631  fproddivf  16008  nfan1c  35109  wl-sbcom2d-lem1  37582  wl-mo2df  37593  wl-eudf  37595  wl-mo3t  37599  wl-ax11-lem4  37611  wl-ax11-lem6  37613