Theorem nfan1 2236

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-12 2213

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

This theorem is used by:  sb4b  2504  ralcom2  3362  sbcralt  3819  sbcrext  3820  csbiebt  3876  riota5f  7394  axrepndlem1  10634  axrepndlem2  10635  axunnd  10638  axpowndlem2  10640  axpowndlem3  10641  axpowndlem4  10642  axregndlem2  10645  axinfndlem1  10647  axinfnd  10648  axacndlem4  10652  axacndlem5  10653  axacnd  10654  fproddivf  16107  nfan1c  35623  axtcond  37182  mh-setindnd  37241  wl-sbcom2d-lem1  38405  wl-mo2df  38416  wl-eudf  38418  wl-mo3t  38422