Theorem nfan1 2056

Description: A closed form of nfan 1816. (Contributed by Mario Carneiro, 3-Oct-2016.) df-nf 1701 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 1767	. . . . 5 ⊢ (Ⅎ𝑥𝜓 → Ⅎ𝑥 ¬ 𝜓)
5	3, 4	syl 17	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜓)
6	2, 5	nfim1 2055	. . 3 ⊢ Ⅎ𝑥(𝜑 → ¬ 𝜓)
7	6	nfn 1768	. 2 ⊢ Ⅎ𝑥 ¬ (𝜑 → ¬ 𝜓)
8	1, 7	nfxfr 1771	1 ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-ex 1696  df-nf 1701

This theorem is referenced by:  ralcom2  3083  sbcralt  3477  sbcrext  3478  sbcrextOLD  3479  csbiebt  3519  riota5f  6535  axrepndlem1  9293  axrepndlem2  9294  axunnd  9297  axpowndlem2  9299  axpowndlem3  9300  axpowndlem4  9301  axregndlem2  9304  axinfndlem1  9306  axinfnd  9307  axacndlem4  9311  axacndlem5  9312  axacnd  9313  fproddivf  14557  wl-sbcom2d-lem1  32521  wl-mo2df  32531  wl-eudf  32533  wl-mo3t  32537  wl-ax11-lem4  32544  wl-ax11-lem6  32546