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 2907  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 2732

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 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-if 4483

This theorem is used by:  csbif  4540  nfop  4849  nfrdg  8403  boxcutc  8948  nfoi  9486  nfsum1  15777  nfsum  15778  summolem2a  15801  zsum  15804  sumss  15810  sumss2  15812  fsumcvg2  15813  nfcprod  15998  cbvprod  16002  prodmolem2a  16021  zprod  16024  fprod  16028  fprodntriv  16029  prodss  16034  pcmpt  16984  pcmptdvds  16986  gsummpt1n0  20092  madugsum  22865  mbfpos  25879  mbfposb  25881  i1fposd  25935  isibl2  25994  nfitg  26002  cbvitg  26003  itgss3  26042  itgcn  26072  limcmpt  26110  rlimcnp2  27203  nosupbnd2  27952  noinfbnd2  27967  chirred  32876  cdleme31sn  41253  cdleme32d  41317  cdleme32f  41319  refsum2cn  45872  ssfiunibd  46142  uzub  46259  limsupubuz  46541  icccncfext  46715  fourierdlem86  47020  vonicc  47513  nfafv  48024  nfafv2  48106