Theorem nfif 4509

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	⊢ Ⅎ𝑥if(𝜑, 𝐴, 𝐵)

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 4508	. 2 ⊢ (⊤ → Ⅎ𝑥if(𝜑, 𝐴, 𝐵))
8	7	mptru 1547	1 ⊢ Ⅎ𝑥if(𝜑, 𝐴, 𝐵)

Syntax hints:  ⊤wtru 1541  Ⅎwnf 1783  Ⅎwnfc 2876  ifcif 4478

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-if 4479

This theorem is referenced by:  csbif  4536  nfop  4843  nfrdg  8343  boxcutc  8875  nfoi  9425  nfsum1  15615  nfsum  15616  summolem2a  15640  zsum  15643  sumss  15649  sumss2  15651  fsumcvg2  15652  nfcprod  15834  cbvprod  15838  prodmolem2a  15859  zprod  15862  fprod  15866  fprodntriv  15867  prodss  15872  pcmpt  16822  pcmptdvds  16824  gsummpt1n0  19862  madugsum  22546  mbfpos  25568  mbfposb  25570  i1fposd  25624  isibl2  25683  nfitg  25692  cbvitg  25693  itgss3  25732  itgcn  25762  limcmpt  25800  rlimcnp2  26892  nosupbnd2  27644  noinfbnd2  27659  chirred  32357  cdleme31sn  40362  cdleme32d  40426  cdleme32f  40428  refsum2cn  45019  ssfiunibd  45294  uzub  45414  limsupubuz  45698  icccncfext  45872  fourierdlem86  46177  vonicc  46670  nfafv  47124  nfafv2  47206