Theorem nfan1 2188

Description: A closed form of nfan 1894. (Contributed by Mario Carneiro, 3-Oct-2016.) df-nf 1778 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 395	. 2 ⊢ ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))
2		nfim1.1	. . . 4 ⊢ Ⅎ𝑥𝜑
3		nfim1.2	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜓)
4	3	nfnd 1853	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜓)
5	2, 4	nfim1 2187	. . 3 ⊢ Ⅎ𝑥(𝜑 → ¬ 𝜓)
6	5	nfn 1852	. 2 ⊢ Ⅎ𝑥 ¬ (𝜑 → ¬ 𝜓)
7	1, 6	nfxfr 1847	1 ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 394  Ⅎwnf 1777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-12 2166

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-ex 1774  df-nf 1778

This theorem is referenced by:  sb4b  2468  ralcom2  3360  sbcralt  3862  sbcrext  3863  csbiebt  3919  riota5f  7404  axrepndlem1  10617  axrepndlem2  10618  axunnd  10621  axpowndlem2  10623  axpowndlem3  10624  axpowndlem4  10625  axregndlem2  10628  axinfndlem1  10630  axinfnd  10631  axacndlem4  10635  axacndlem5  10636  axacnd  10637  fproddivf  15967  wl-sbcom2d-lem1  37157  wl-mo2df  37168  wl-eudf  37170  wl-mo3t  37174  wl-ax11-lem4  37186  wl-ax11-lem6  37188