Theorem nfan1

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

	Ref	Expression
Hypotheses	nfim1.1	$$⊢Ⅎx\phi$$
	nfim1.2	$$⊢\phi \to Ⅎx\psi$$
Assertion	nfan1	$$⊢Ⅎx\left(\phi \wedge \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		nfim1.1	$$⊢Ⅎx\phi$$
2		nfim1.2	$$⊢\phi \to Ⅎx\psi$$
3		df-an	$$⊢\left(\phi \wedge \psi \right)\leftrightarrow \neg \left(\phi \to \neg \psi \right)$$
4	2	nfnd	$$⊢\phi \to Ⅎx\neg \psi$$
5	1 4	nfim1	$$⊢Ⅎx\left(\phi \to \neg \psi \right)$$
6	5	nfn	$$⊢Ⅎx\neg \left(\phi \to \neg \psi \right)$$
7	3 6	nfxfr	$$⊢Ⅎx\left(\phi \wedge \psi \right)$$