Theorem nfan1 2196

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-12 2173

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

This theorem is referenced by:  sb4b  2495  sb4bOLD  2496  ralcom2  3363  sbcralt  3854  sbcrext  3855  csbiebt  3911  riota5f  7136  axrepndlem1  10008  axrepndlem2  10009  axunnd  10012  axpowndlem2  10014  axpowndlem3  10015  axpowndlem4  10016  axregndlem2  10019  axinfndlem1  10021  axinfnd  10022  axacndlem4  10026  axacndlem5  10027  axacnd  10028  fproddivf  15335  wl-sbcom2d-lem1  34789  wl-mo2df  34800  wl-eudf  34802  wl-mo3t  34806  wl-ax11-lem4  34814  wl-ax11-lem6  34816