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	⊢ Ⅎ 𝑥 𝜑
	nfan.2	⊢ Ⅎ 𝑥 𝜓
Assertion	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		nfan.1	⊢ Ⅎ 𝑥 𝜑
2		nfan.2	⊢ Ⅎ 𝑥 𝜓
3	1	a1i	⊢ ( ⊤ → Ⅎ 𝑥 𝜑 )
4	2	a1i	⊢ ( ⊤ → Ⅎ 𝑥 𝜓 )
5	3 4	nfand	⊢ ( ⊤ → Ⅎ 𝑥 ( 𝜑 ∧ 𝜓 ) )
6	5	mptru	⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝜓 )