Theorem nfif 3576

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

Hypotheses

Ref	Expression
nfif.1	|- F/ x ph
nfif.2	|- F/_ x A
nfif.3	|- F/_ x B

Assertion

Ref	Expression
nfif	|- F/_ x if ( ph , A , B )

Proof of Theorem nfif

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

Syntax hints:   T. wtru 1364   F/wnf 1470   F/_wnfc 2318   ifcif 3548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2170

This theorem depends on definitions:  df-bi 117  df-tru 1366  df-fal 1369  df-nf 1471  df-sb 1773  df-clab 2175  df-cleq 2181  df-clel 2184  df-nfc 2320  df-if 3549

This theorem is referenced by:  nfsum1  11381  nfsum  11382  sumrbdclem  11402  summodclem2a  11406  zsumdc  11409  fsum3  11412  isumss  11416  isumss2  11418  fsum3cvg2  11419  nfcprod1  11579  nfcprod  11580  cbvprod  11583  prodrbdclem  11596  prodmodclem2a  11601  zproddc  11604  fprodseq  11608  fprodntrivap  11609  prodssdc  11614  pcmpt  12358  pcmptdvds  12360