Theorem nfan1 2237

Description: A closed form of nfan 1921. (Contributed by Mario Carneiro, 3-Oct-2016.) df-nf 1806 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 400	. 2 ⊢ ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))
2		nfim1.1	. . . 4 ⊢ Ⅎ𝑥𝜑
3		nfim1.2	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜓)
4	3	nfnd 1880	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜓)
5	2, 4	nfim1 2236	. . 3 ⊢ Ⅎ𝑥(𝜑 → ¬ 𝜓)
6	5	nfn 1879	. 2 ⊢ Ⅎ𝑥 ¬ (𝜑 → ¬ 𝜓)
7	1, 6	nfxfr 1875	1 ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399  Ⅎwnf 1805

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-12 2214

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-ex 1802  df-nf 1806

This theorem is referenced by:  sb4b  2508  ralcom2  3366  sbcralt  3827  sbcrext  3828  csbiebt  3883  riota5f  7383  axrepndlem1  10552  axrepndlem2  10553  axunnd  10556  axpowndlem2  10558  axpowndlem3  10559  axpowndlem4  10560  axregndlem2  10563  axinfndlem1  10565  axinfnd  10566  axacndlem4  10570  axacndlem5  10571  axacnd  10572  fproddivf  16019  nfan1c  35370  axtcond  36843  mh-setindnd  36902  wl-sbcom2d-lem1  38067  wl-mo2df  38078  wl-eudf  38080  wl-mo3t  38084