Theorem nfan1 2235

Description: A closed form of nfan 1928. (Contributed by Mario Carneiro, 3-Oct-2016.) df-nf 1813 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 401	. 2 ⊢ ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))
2		nfim1.1	. . . 4 ⊢ Ⅎ𝑥𝜑
3		nfim1.2	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜓)
4	3	nfnd 1887	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜓)
5	2, 4	nfim1 2234	. . 3 ⊢ Ⅎ𝑥(𝜑 → ¬ 𝜓)
6	5	nfn 1886	. 2 ⊢ Ⅎ𝑥 ¬ (𝜑 → ¬ 𝜓)
7	1, 6	nfxfr 1882	1 ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓)

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-12 2212

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1809  df-nf 1813

This theorem is used by:  sb4b  2506  ralcom2  3365  sbcralt  3824  sbcrext  3825  csbiebt  3881  riota5f  7397  axrepndlem1  10583  axrepndlem2  10584  axunnd  10587  axpowndlem2  10589  axpowndlem3  10590  axpowndlem4  10591  axregndlem2  10594  axinfndlem1  10596  axinfnd  10597  axacndlem4  10601  axacndlem5  10602  axacnd  10603  fproddivf  16048  nfan1c  35470  axtcond  37017  mh-setindnd  37076  wl-sbcom2d-lem1  38242  wl-mo2df  38253  wl-eudf  38255  wl-mo3t  38259