Theorem nfan1 2200

Description: A closed form of nfan 1900. (Contributed by Mario Carneiro, 3-Oct-2016.) df-nf 1785 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 399	. 2 ⊢ ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))
2		nfim1.1	. . . 4 ⊢ Ⅎ𝑥𝜑
3		nfim1.2	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜓)
4	3	nfnd 1858	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜓)
5	2, 4	nfim1 2199	. . 3 ⊢ Ⅎ𝑥(𝜑 → ¬ 𝜓)
6	5	nfn 1857	. 2 ⊢ Ⅎ𝑥 ¬ (𝜑 → ¬ 𝜓)
7	1, 6	nfxfr 1853	1 ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398  Ⅎwnf 1784

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-12 2177

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1781  df-nf 1785

This theorem is referenced by:  sb4b  2499  sb4bOLD  2500  ralcom2  3363  sbcralt  3844  sbcrext  3845  csbiebt  3900  riota5f  7128  axrepndlem1  10000  axrepndlem2  10001  axunnd  10004  axpowndlem2  10006  axpowndlem3  10007  axpowndlem4  10008  axregndlem2  10011  axinfndlem1  10013  axinfnd  10014  axacndlem4  10018  axacndlem5  10019  axacnd  10020  fproddivf  15326  wl-sbcom2d-lem1  34829  wl-mo2df  34840  wl-eudf  34842  wl-mo3t  34846  wl-ax11-lem4  34854  wl-ax11-lem6  34856