Theorem nfan1 2194

Description: A closed form of nfan 1903. (Contributed by Mario Carneiro, 3-Oct-2016.) df-nf 1787 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 398	. 2 ⊢ ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))
2		nfim1.1	. . . 4 ⊢ Ⅎ𝑥𝜑
3		nfim1.2	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜓)
4	3	nfnd 1862	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜓)
5	2, 4	nfim1 2193	. . 3 ⊢ Ⅎ𝑥(𝜑 → ¬ 𝜓)
6	5	nfn 1861	. 2 ⊢ Ⅎ𝑥 ¬ (𝜑 → ¬ 𝜓)
7	1, 6	nfxfr 1856	1 ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 397  Ⅎwnf 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2172

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-nf 1787

This theorem is referenced by:  sb4b  2475  ralcom2  3374  sbcralt  3867  sbcrext  3868  csbiebt  3924  riota5f  7394  axrepndlem1  10587  axrepndlem2  10588  axunnd  10591  axpowndlem2  10593  axpowndlem3  10594  axpowndlem4  10595  axregndlem2  10598  axinfndlem1  10600  axinfnd  10601  axacndlem4  10605  axacndlem5  10606  axacnd  10607  fproddivf  15931  wl-sbcom2d-lem1  36424  wl-mo2df  36435  wl-eudf  36437  wl-mo3t  36441  wl-ax11-lem4  36450  wl-ax11-lem6  36452