Theorem nfan1 2238

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 2237	. . 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 2215

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  2506  ralcom2  3364  sbcralt  3822  sbcrext  3823  csbiebt  3879  riota5f  7401  axrepndlem1  10604  axrepndlem2  10605  axunnd  10608  axpowndlem2  10610  axpowndlem3  10611  axpowndlem4  10612  axregndlem2  10615  axinfndlem1  10617  axinfnd  10618  axacndlem4  10622  axacndlem5  10623  axacnd  10624  fproddivf  16078  nfan1c  35569  axtcond  37084  mh-setindnd  37143  wl-sbcom2d-lem1  38309  wl-mo2df  38320  wl-eudf  38322  wl-mo3t  38326