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
|- F/ x ph
nfif.2
|- F/_ x A
nfif.3
|- F/_ x B
Assertion nfif
|- F/_ x if ( ph , A , B )

Proof

Step Hyp Ref Expression
1 nfif.1
 |-  F/ x ph
2 nfif.2
 |-  F/_ x A
3 nfif.3
 |-  F/_ x B
4 1 a1i
 |-  ( T. -> F/ x ph )
5 2 a1i
 |-  ( T. -> F/_ x A )
6 3 a1i
 |-  ( T. -> F/_ x B )
7 4 5 6 nfifd
 |-  ( T. -> F/_ x if ( ph , A , B ) )
8 7 mptru
 |-  F/_ x if ( ph , A , B )