Theorem nfan1 2242

Description: A closed form of nfan 1926. (Contributed by Mario Carneiro, 3-Oct-2016.) df-nf 1811 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 1885	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜓)
5	2, 4	nfim1 2241	. . 3 ⊢ Ⅎ𝑥(𝜑 → ¬ 𝜓)
6	5	nfn 1884	. 2 ⊢ Ⅎ𝑥 ¬ (𝜑 → ¬ 𝜓)
7	1, 6	nfxfr 1880	1 ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400  Ⅎwnf 1810

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-12 2219

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1807  df-nf 1811

This theorem is referenced by:  sb4b  2513  ralcom2  3372  sbcralt  3832  sbcrext  3833  csbiebt  3888  riota5f  7396  axrepndlem1  10577  axrepndlem2  10578  axunnd  10581  axpowndlem2  10583  axpowndlem3  10584  axpowndlem4  10585  axregndlem2  10588  axinfndlem1  10590  axinfnd  10591  axacndlem4  10595  axacndlem5  10596  axacnd  10597  fproddivf  16041  nfan1c  35406  axtcond  36912  mh-setindnd  36971  wl-sbcom2d-lem1  38137  wl-mo2df  38148  wl-eudf  38150  wl-mo3t  38154