Theorem nfov

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

	Ref	Expression
Hypotheses	nfov.1	$$⊢\underset{\_}{Ⅎ}xA$$
	nfov.2	$$⊢\underset{\_}{Ⅎ}xF$$
	nfov.3	$$⊢\underset{\_}{Ⅎ}xB$$
Assertion	nfov	$$⊢\underset{\_}{Ⅎ}x\left(AFB\right)$$

Proof

Step	Hyp	Ref	Expression
1		nfov.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		nfov.2	$$⊢\underset{\_}{Ⅎ}xF$$
3		nfov.3	$$⊢\underset{\_}{Ⅎ}xB$$
4	1	a1i	$$⊢\top \to \underset{\_}{Ⅎ}xA$$
5	2	a1i	$$⊢\top \to \underset{\_}{Ⅎ}xF$$
6	3	a1i	$$⊢\top \to \underset{\_}{Ⅎ}xB$$
7	4 5 6	nfovd	$$⊢\top \to \underset{\_}{Ⅎ}x\left(AFB\right)$$
8	7	mptru	$$⊢\underset{\_}{Ⅎ}x\left(AFB\right)$$