# Metamath Proof Explorer

## Theorem nfov

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

Ref Expression
Hypotheses nfov.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
nfov.2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}$
nfov.3 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}$
Assertion nfov ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({A}{F}{B}\right)$

### Proof

Step Hyp Ref Expression
1 nfov.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
2 nfov.2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}$
3 nfov.3 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}$
4 1 a1i ${⊢}\top \to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
5 2 a1i ${⊢}\top \to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}$
6 3 a1i ${⊢}\top \to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}$
7 4 5 6 nfovd ${⊢}\top \to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({A}{F}{B}\right)$
8 7 mptru ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({A}{F}{B}\right)$