Theorem nfan1 2206

Description: A closed form of nfan 1901. (Contributed by Mario Carneiro, 3-Oct-2016.) df-nf 1786 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 396	. 2 ⊢ ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))
2		nfim1.1	. . . 4 ⊢ Ⅎ𝑥𝜑
3		nfim1.2	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜓)
4	3	nfnd 1860	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜓)
5	2, 4	nfim1 2205	. . 3 ⊢ Ⅎ𝑥(𝜑 → ¬ 𝜓)
6	5	nfn 1859	. 2 ⊢ Ⅎ𝑥 ¬ (𝜑 → ¬ 𝜓)
7	1, 6	nfxfr 1855	1 ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395  Ⅎwnf 1785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-12 2183

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-nf 1786

This theorem is referenced by:  sb4b  2478  ralcom2  3346  sbcralt  3821  sbcrext  3822  csbiebt  3877  riota5f  7343  axrepndlem1  10505  axrepndlem2  10506  axunnd  10509  axpowndlem2  10511  axpowndlem3  10512  axpowndlem4  10513  axregndlem2  10516  axinfndlem1  10518  axinfnd  10519  axacndlem4  10523  axacndlem5  10524  axacnd  10525  fproddivf  15912  nfan1c  35208  wl-sbcom2d-lem1  37733  wl-mo2df  37744  wl-eudf  37746  wl-mo3t  37750