Theorem nfan1 2106

Description: A closed form of nfan 1868. (Contributed by Mario Carneiro, 3-Oct-2016.) df-nf 1750 changed. (Revised by Wolf Lammen, 18-Sep-2021.)

Hypotheses

Ref	Expression
nfim1.1	⊢ Ⅎ𝑥𝜑
nfim1.2	⊢ (𝜑 → Ⅎ𝑥𝜓)

Assertion

Ref	Expression
nfan1	⊢ Ⅎ𝑥(𝜑 ∧ 𝜓)

Proof of Theorem nfan1

Step	Hyp	Ref	Expression
1		df-an 385	. 2 ⊢ ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))
2		nfim1.1	. . . 4 ⊢ Ⅎ𝑥𝜑
3		nfim1.2	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜓)
4		nfnt 1822	. . . . 5 ⊢ (Ⅎ𝑥𝜓 → Ⅎ𝑥 ¬ 𝜓)
5	3, 4	syl 17	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜓)
6	2, 5	nfim1 2105	. . 3 ⊢ Ⅎ𝑥(𝜑 → ¬ 𝜓)
7	6	nfn 1824	. 2 ⊢ Ⅎ𝑥 ¬ (𝜑 → ¬ 𝜓)
8	1, 7	nfxfr 1819	1 ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383  Ⅎwnf 1748

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-12 2087

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-ex 1745  df-nf 1750

This theorem is referenced by:  ralcom2  3133  sbcralt  3543  sbcrext  3544  sbcrextOLD  3545  csbiebt  3586  riota5f  6676  axrepndlem1  9452  axrepndlem2  9453  axunnd  9456  axpowndlem2  9458  axpowndlem3  9459  axpowndlem4  9460  axregndlem2  9463  axinfndlem1  9465  axinfnd  9466  axacndlem4  9470  axacndlem5  9471  axacnd  9472  fproddivf  14762  wl-sbcom2d-lem1  33472  wl-mo2df  33482  wl-eudf  33484  wl-mo3t  33488  wl-ax11-lem4  33495  wl-ax11-lem6  33497