Theorem nfan1c

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

	Ref	Expression
Hypotheses	nfan1c.1	|- F/ x ph
	nfan1c.2	|- ( ph -> F/ x ps )
Assertion	nfan1c	|- F/ x ( ps /\ ph )

Proof

Step	Hyp	Ref	Expression
1		nfan1c.1	|- F/ x ph
2		nfan1c.2	|- ( ph -> F/ x ps )
3	1 2	nfan1	|- F/ x ( ph /\ ps )
4		ancom	|- ( ( ph /\ ps ) <-> ( ps /\ ph ) )
5	4	nfbii	|- ( F/ x ( ph /\ ps ) <-> F/ x ( ps /\ ph ) )
6	3 5	mpbi	|- F/ x ( ps /\ ph )