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  7402  axrepndlem1  10605  axrepndlem2  10606  axunnd  10609  axpowndlem2  10611  axpowndlem3  10612  axpowndlem4  10613  axregndlem2  10616  axinfndlem1  10618  axinfnd  10619  axacndlem4  10623  axacndlem5  10624  axacnd  10625  fproddivf  16080  nfan1c  35590  axtcond  37105  mh-setindnd  37164  wl-sbcom2d-lem1  38330  wl-mo2df  38341  wl-eudf  38343  wl-mo3t  38347