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  8404  boxcutc  8951  nfoi  9489  nfsum1  15780  nfsum  15781  summolem2a  15804  zsum  15807  sumss  15813  sumss2  15815  fsumcvg2  15816  nfcprod  16001  cbvprod  16005  prodmolem2a  16024  zprod  16027  fprod  16031  fprodntriv  16032  prodss  16037  pcmpt  16987  pcmptdvds  16989  gsummpt1n0  20095  madugsum  22868  mbfpos  25882  mbfposb  25884  i1fposd  25938  isibl2  25997  nfitg  26005  cbvitg  26006  itgss3  26045  itgcn  26075  limcmpt  26113  rlimcnp2  27206  nosupbnd2  27955  noinfbnd2  27970  chirred  32879  cdleme31sn  41256  cdleme32d  41320  cdleme32f  41322  refsum2cn  45875  ssfiunibd  46145  uzub  46262  limsupubuz  46544  icccncfext  46718  fourierdlem86  47023  vonicc  47516  nfafv  48027  nfafv2  48109