Theorem nfan1 2196

Description: A closed form of nfan 1903. (Contributed by Mario Carneiro, 3-Oct-2016.) df-nf 1788 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 1862	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜓)
5	2, 4	nfim1 2195	. . 3 ⊢ Ⅎ𝑥(𝜑 → ¬ 𝜓)
6	5	nfn 1861	. 2 ⊢ Ⅎ𝑥 ¬ (𝜑 → ¬ 𝜓)
7	1, 6	nfxfr 1856	1 ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2173

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-ex 1784  df-nf 1788

This theorem is referenced by:  sb4b  2475  sb4bOLD  2476  ralcom2  3288  sbcralt  3801  sbcrext  3802  csbiebt  3858  riota5f  7241  axrepndlem1  10279  axrepndlem2  10280  axunnd  10283  axpowndlem2  10285  axpowndlem3  10286  axpowndlem4  10287  axregndlem2  10290  axinfndlem1  10292  axinfnd  10293  axacndlem4  10297  axacndlem5  10298  axacnd  10299  fproddivf  15625  wl-sbcom2d-lem1  35641  wl-mo2df  35652  wl-eudf  35654  wl-mo3t  35658  wl-ax11-lem4  35666  wl-ax11-lem6  35668