Theorem nfan1 2214

Description: A closed form of nfan 1907. (Contributed by Mario Carneiro, 3-Oct-2016.) df-nf 1792 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 398	. 2 ⊢ ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))
2		nfim1.1	. . . 4 ⊢ Ⅎ𝑥𝜑
3		nfim1.2	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜓)
4	3	nfnd 1866	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜓)
5	2, 4	nfim1 2213	. . 3 ⊢ Ⅎ𝑥(𝜑 → ¬ 𝜓)
6	5	nfn 1865	. 2 ⊢ Ⅎ𝑥 ¬ (𝜑 → ¬ 𝜓)
7	1, 6	nfxfr 1861	1 ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 397  Ⅎwnf 1791

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-12 2191

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-ex 1788  df-nf 1792

This theorem is referenced by:  sb4b  2485  ralcom2  3343  sbcralt  3806  sbcrext  3807  csbiebt  3862  riota5f  7345  axrepndlem1  10510  axrepndlem2  10511  axunnd  10514  axpowndlem2  10516  axpowndlem3  10517  axpowndlem4  10518  axregndlem2  10521  axinfndlem1  10523  axinfnd  10524  axacndlem4  10528  axacndlem5  10529  axacnd  10530  fproddivf  15947  nfan1c  35270  axtcond  36721  mh-setindnd  36780  wl-sbcom2d-lem1  37945  wl-mo2df  37956  wl-eudf  37958  wl-mo3t  37962