Theorem nfan1 2236

Description: A closed form of nfan 1931. (Contributed by Mario Carneiro, 3-Oct-2016.) df-nf 1816 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 402	. 2 ⊢ ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))
2		nfim1.1	. . . 4 ⊢ Ⅎ𝑥𝜑
3		nfim1.2	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜓)
4	3	nfnd 1890	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜓)
5	2, 4	nfim1 2235	. . 3 ⊢ Ⅎ𝑥(𝜑 → ¬ 𝜓)
6	5	nfn 1889	. 2 ⊢ Ⅎ𝑥 ¬ (𝜑 → ¬ 𝜓)
7	1, 6	nfxfr 1885	1 ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401  Ⅎwnf 1815

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-12 2212

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1812  df-nf 1816

This theorem is used by:  sb4b  2504  ralcom2  3362  sbcralt  3818  sbcrext  3819  csbiebt  3875  riota5f  7405  axrepndlem1  10677  axrepndlem2  10678  axunnd  10681  axpowndlem2  10683  axpowndlem3  10684  axpowndlem4  10685  axregndlem2  10688  axinfndlem1  10690  axinfnd  10691  axacndlem4  10695  axacndlem5  10696  axacnd  10697  fproddivf  16154  nfan1c  35703  axtcond  37266  mh-setindnd  37325  wl-sbcom2d-lem1  38492  wl-mo2df  38503  wl-eudf  38505  wl-mo3t  38509