Theorem nfif 4497

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

Syntax hints:  ⊤wtru 1543  Ⅎwnf 1785  Ⅎwnfc 2883  ifcif 4466

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-if 4467

This theorem is referenced by:  csbif  4524  nfop  4832  nfrdg  8353  boxcutc  8889  nfoi  9429  nfsum1  15652  nfsum  15653  summolem2a  15677  zsum  15680  sumss  15686  sumss2  15688  fsumcvg2  15689  nfcprod  15874  cbvprod  15878  prodmolem2a  15899  zprod  15902  fprod  15906  fprodntriv  15907  prodss  15912  pcmpt  16863  pcmptdvds  16865  gsummpt1n0  19940  madugsum  22608  mbfpos  25618  mbfposb  25620  i1fposd  25674  isibl2  25733  nfitg  25742  cbvitg  25743  itgss3  25782  itgcn  25812  limcmpt  25850  rlimcnp2  26930  nosupbnd2  27680  noinfbnd2  27695  chirred  32466  cdleme31sn  40826  cdleme32d  40890  cdleme32f  40892  refsum2cn  45469  ssfiunibd  45742  uzub  45859  limsupubuz  46141  icccncfext  46315  fourierdlem86  46620  vonicc  47113  nfafv  47584  nfafv2  47666