Theorem nfif 4513

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

This proof depends on syntax axioms:  ⊤wtru 1571  Ⅎwnf 1816  Ⅎwnfc 2908  ifcif 4482

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-if 4483

This theorem is used by:  csbif  4540  nfop  4849  nfrdg  8415  boxcutc  8962  nfoi  9501  nfsum1  15850  nfsum  15851  summolem2a  15874  zsum  15877  sumss  15883  sumss2  15885  fsumcvg2  15886  nfcprod  16071  cbvprod  16075  prodmolem2a  16094  zprod  16097  fprod  16101  fprodntriv  16102  prodss  16107  pcmpt  17063  pcmptdvds  17065  gsummpt1n0  20172  madugsum  22951  mbfpos  25965  mbfposb  25967  i1fposd  26021  isibl2  26080  nfitg  26088  cbvitg  26089  itgss3  26128  itgcn  26158  limcmpt  26196  rlimcnp2  27287  nosupbnd2  28066  noinfbnd2  28081  chirred  32990  cdleme31sn  41417  cdleme32d  41481  cdleme32f  41483  refsum2cn  46024  ssfiunibd  46294  uzub  46410  limsupubuz  46692  icccncfext  46866  fourierdlem86  47171  vonicc  47664  nfafv  48175  nfafv2  48257