Theorem nfan

Description: If x is not free in ph and ps , then it is not free in ( ph /\ ps ) . (Contributed by Mario Carneiro, 11-Aug-2016) (Proof shortened by Wolf Lammen, 13-Jan-2018) (Proof shortened by Wolf Lammen, 9-Oct-2021)

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

Proof

Step	Hyp	Ref	Expression
1		nfan.1	$$⊢Ⅎx\phi$$
2		nfan.2	$$⊢Ⅎx\psi$$
3	1	a1i	$$⊢\top \to Ⅎx\phi$$
4	2	a1i	$$⊢\top \to Ⅎx\psi$$
5	3 4	nfand	$$⊢\top \to Ⅎx\left(\phi \wedge \psi \right)$$
6	5	mptru	$$⊢Ⅎx\left(\phi \wedge \psi \right)$$