Theorem nfif 4514

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

Syntax hints:  ⊤wtru 1564  Ⅎwnf 1806  Ⅎwnfc 2912  ifcif 4483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-nf 1807  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-if 4484

This theorem is referenced by:  csbif  4541  nfop  4849  nfrdg  8389  boxcutc  8927  nfoi  9464  nfsum1  15729  nfsum  15730  summolem2a  15754  zsum  15757  sumss  15763  sumss2  15765  fsumcvg2  15766  nfcprod  15951  cbvprod  15955  prodmolem2a  15976  zprod  15979  fprod  15983  fprodntriv  15984  prodss  15989  pcmpt  16940  pcmptdvds  16942  gsummpt1n0  20023  madugsum  22757  mbfpos  25767  mbfposb  25769  i1fposd  25823  isibl2  25882  nfitg  25891  cbvitg  25892  itgss3  25931  itgcn  25961  limcmpt  25999  rlimcnp2  27085  nosupbnd2  27834  noinfbnd2  27849  chirred  32652  cdleme31sn  41011  cdleme32d  41075  cdleme32f  41077  refsum2cn  45617  ssfiunibd  45887  uzub  46004  limsupubuz  46286  icccncfext  46460  fourierdlem86  46765  vonicc  47258  nfafv  47729  nfafv2  47811