Theorem bj-nnfth

Description: A variable is nonfree in a theorem, inference form. (Contributed by BJ, 28-Jul-2023)

	Ref	Expression
Hypothesis	bj-nnfth.1	|- ph
Assertion	bj-nnfth	|- F// x ph

Proof

Step	Hyp	Ref	Expression
1		bj-nnfth.1	|- ph
2		bj-nnftht	|- ( ( ph /\ A. x ph ) -> F// x ph )
3	1 2	bj-mpgs	|- F// x ph