Theorem nfan1 2198

Description: A closed form of nfan 1900. (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 400	. 2 ⊢ ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))
2		nfim1.1	. . . 4 ⊢ Ⅎ𝑥𝜑
3		nfim1.2	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜓)
4	3	nfnd 1859	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜓)
5	2, 4	nfim1 2197	. . 3 ⊢ Ⅎ𝑥(𝜑 → ¬ 𝜓)
6	5	nfn 1858	. 2 ⊢ Ⅎ𝑥 ¬ (𝜑 → ¬ 𝜓)
7	1, 6	nfxfr 1854	1 ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399  Ⅎ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 1911  ax-6 1970  ax-7 2015  ax-12 2175

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786

This theorem is referenced by:  sb4b  2488  sb4bOLD  2489  ralcom2  3316  sbcralt  3801  sbcrext  3802  csbiebt  3857  riota5f  7121  axrepndlem1  10003  axrepndlem2  10004  axunnd  10007  axpowndlem2  10009  axpowndlem3  10010  axpowndlem4  10011  axregndlem2  10014  axinfndlem1  10016  axinfnd  10017  axacndlem4  10021  axacndlem5  10022  axacnd  10023  fproddivf  15333  wl-sbcom2d-lem1  34960  wl-mo2df  34971  wl-eudf  34973  wl-mo3t  34977  wl-ax11-lem4  34985  wl-ax11-lem6  34987