Theorem nfif 4115

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 11	. . 3 |- ( T. -> F/ x ph )
3		nfif.2	. . . 4 |- F/_ x A
4	3	a1i 11	. . 3 |- ( T. -> F/_ x A )
5		nfif.3	. . . 4 |- F/_ x B
6	5	a1i 11	. . 3 |- ( T. -> F/_ x B )
7	2, 4, 6	nfifd 4114	. 2 |- ( T. -> F/_ x if ( ph , A , B ) )
8	7	trud 1493	1 |- F/_ x if ( ph , A , B )

Syntax hints:   T. wtru 1484   F/wnf 1708   F/_wnfc 2751   ifcif 4086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-if 4087

This theorem is referenced by:  csbif  4138  nfop  4418  nfrdg  7510  boxcutc  7951  nfoi  8419  nfsum1  14420  nfsum  14421  summolem2a  14446  zsum  14449  sumss  14455  sumss2  14457  fsumcvg2  14458  nfcprod  14641  cbvprod  14645  prodmolem2a  14664  zprod  14667  fprod  14671  fprodntriv  14672  prodss  14677  pcmpt  15596  pcmptdvds  15598  gsummpt1n0  18364  madugsum  20449  mbfpos  23418  mbfposb  23420  i1fposd  23474  isibl2  23533  nfitg  23541  cbvitg  23542  itgss3  23581  itgcn  23609  limcmpt  23647  rlimcnp2  24693  chirred  29254  nosupbnd2  31862  cdleme31sn  35668  cdleme32d  35732  cdleme32f  35734  refsum2cn  39197  ssfiunibd  39523  uzub  39658  limsupubuz  39945  icccncfext  40100  fourierdlem86  40409  vonicc  40899  nfafv  41216