Theorem nfan1 2182

Description: A closed form of nfan 1946. (Contributed by Mario Carneiro, 3-Oct-2016.) df-nf 1828 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 387	. 2 ⊢ ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))
2		nfim1.1	. . . 4 ⊢ Ⅎ𝑥𝜑
3		nfim1.2	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜓)
4	3	nfnd 1903	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜓)
5	2, 4	nfim1 2181	. . 3 ⊢ Ⅎ𝑥(𝜑 → ¬ 𝜓)
6	5	nfn 1902	. 2 ⊢ Ⅎ𝑥 ¬ (𝜑 → ¬ 𝜓)
7	1, 6	nfxfr 1897	1 ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 386  Ⅎwnf 1827

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-12 2162

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-ex 1824  df-nf 1828

This theorem is referenced by:  ralcom2  3289  sbcralt  3727  sbcrext  3728  csbiebt  3770  riota5f  6908  axrepndlem1  9749  axrepndlem2  9750  axunnd  9753  axpowndlem2  9755  axpowndlem3  9756  axpowndlem4  9757  axregndlem2  9760  axinfndlem1  9762  axinfnd  9763  axacndlem4  9767  axacndlem5  9768  axacnd  9769  fproddivf  15120  wl-sbcom2d-lem1  33950  wl-mo2df  33960  wl-eudf  33962  wl-mo3t  33966  wl-ax11-lem4  33973  wl-ax11-lem6  33975