Theorem nfif 4520

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

This proof depends on syntax axioms:  ⊤wtru 1571  Ⅎwnf 1816  Ⅎwnfc 2912  ifcif 4489

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-if 4490

This theorem is used by:  csbif  4547  nfop  4856  nfrdg  8403  boxcutc  8941  nfoi  9479  nfsum1  15760  nfsum  15761  summolem2a  15784  zsum  15787  sumss  15793  sumss2  15795  fsumcvg2  15796  nfcprod  15981  cbvprod  15985  prodmolem2a  16006  zprod  16009  fprod  16013  fprodntriv  16014  prodss  16019  pcmpt  16969  pcmptdvds  16971  gsummpt1n0  20058  madugsum  22829  mbfpos  25839  mbfposb  25841  i1fposd  25895  isibl2  25954  nfitg  25963  cbvitg  25964  itgss3  26003  itgcn  26033  limcmpt  26071  rlimcnp2  27160  nosupbnd2  27909  noinfbnd2  27924  chirred  32776  cdleme31sn  41187  cdleme32d  41251  cdleme32f  41253  refsum2cn  45791  ssfiunibd  46061  uzub  46178  limsupubuz  46460  icccncfext  46634  fourierdlem86  46939  vonicc  47432  nfafv  47906  nfafv2  47988