Theorem nfov

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

	Ref	Expression
Hypotheses	nfov.1	⊢ Ⅎ 𝑥 𝐴
	nfov.2	⊢ Ⅎ 𝑥 𝐹
	nfov.3	⊢ Ⅎ 𝑥 𝐵
Assertion	nfov	⊢ Ⅎ 𝑥 ( 𝐴 𝐹 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		nfov.1	⊢ Ⅎ 𝑥 𝐴
2		nfov.2	⊢ Ⅎ 𝑥 𝐹
3		nfov.3	⊢ Ⅎ 𝑥 𝐵
4	1	a1i	⊢ ( ⊤ → Ⅎ 𝑥 𝐴 )
5	2	a1i	⊢ ( ⊤ → Ⅎ 𝑥 𝐹 )
6	3	a1i	⊢ ( ⊤ → Ⅎ 𝑥 𝐵 )
7	4 5 6	nfovd	⊢ ( ⊤ → Ⅎ 𝑥 ( 𝐴 𝐹 𝐵 ) )
8	7	mptru	⊢ Ⅎ 𝑥 ( 𝐴 𝐹 𝐵 )