Theorem nfov

Description: Bound-variable hypothesis builder for operation value. (Contributed by NM, 4-May-2004)

	Ref	Expression
Hypotheses	nfov.1	|- F/_ x A
	nfov.2	|- F/_ x F
	nfov.3	|- F/_ x B
Assertion	nfov	|- F/_ x ( A F B )

Proof

Step	Hyp	Ref	Expression
1		nfov.1	|- F/_ x A
2		nfov.2	|- F/_ x F
3		nfov.3	|- F/_ x B
4	1	a1i	|- ( T. -> F/_ x A )
5	2	a1i	|- ( T. -> F/_ x F )
6	3	a1i	|- ( T. -> F/_ x B )
7	4 5 6	nfovd	|- ( T. -> F/_ x ( A F B ) )
8	7	mptru	|- F/_ x ( A F B )