# Metamath Proof Explorer

## Theorem nfif

Description: Bound-variable hypothesis builder for a conditional operator. (Contributed by NM, 16-Feb-2005) (Proof shortened by Andrew Salmon, 26-Jun-2011)

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

### Proof

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