Theorem nfan1c

Description: Variant of nfan and commuted form of nfan1 . (Contributed by BTernaryTau, 31-Jul-2025)

	Ref	Expression
Hypotheses	nfan1c.1	⊢ Ⅎ 𝑥 𝜑
	nfan1c.2	⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 )
Assertion	nfan1c	⊢ Ⅎ 𝑥 ( 𝜓 ∧ 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		nfan1c.1	⊢ Ⅎ 𝑥 𝜑
2		nfan1c.2	⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 )
3	1 2	nfan1	⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝜓 )
4		ancom	⊢ ( ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜓 ∧ 𝜑 ) )
5	4	nfbii	⊢ ( Ⅎ 𝑥 ( 𝜑 ∧ 𝜓 ) ↔ Ⅎ 𝑥 ( 𝜓 ∧ 𝜑 ) )
6	3 5	mpbi	⊢ Ⅎ 𝑥 ( 𝜓 ∧ 𝜑 )