Theorem nfif 3970

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
nfif.2
nfif.3

Assertion

Ref	Expression
nfif

Proof of Theorem nfif

Step	Hyp	Ref	Expression
1		nfif.1	. . . 4
2	1	a1i 11	. . 3
3		nfif.2	. . . 4
4	3	a1i 11	. . 3
5		nfif.3	. . . 4
6	5	a1i 11	. . 3
7	2, 4, 6	nfifd 3969	. 2
8	7	trud 1404	1

Syntax hints:  wtru 1396  F/wnf 1616  F/_wnfc 2605  ifcif 3941

This theorem is referenced by:  csbif  3991  csbifgOLD  3992  nfop  4233  nfrdg  7099  boxcutc  7532  nfoi  7960  nfsum1  13512  nfsum  13513  summolem2a  13537  zsum  13540  sumss  13546  sumss2  13548  fsumcvg2  13549  nfcprod  13718  cbvprod  13722  prodmolem2a  13741  zprod  13744  fprod  13748  fprodntriv  13749  prodss  13754  pcmpt  14411  pcmptdvds  14413  gsummpt1n0  16992  madugsum  19145  mbfpos  22058  mbfposb  22060  i1fposd  22114  isibl2  22173  nfitg  22181  cbvitg  22182  itgss3  22221  itgcn  22249  limcmpt  22287  rlimcnp2  23296  chirred  27314  refsum2cn  31413  ssfiunibd  31509  icccncfext  31690  fourierdlem86  31975  nfafv  32221  cdleme31sn  36106  cdleme32d  36170  cdleme32f  36172

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-if 3942