Theorem nfif 4489

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

Syntax hints:  ⊤wtru 1537  Ⅎwnf 1783  Ⅎwnfc 2960  ifcif 4460

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2792

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2799  df-cleq 2813  df-clel 2892  df-nfc 2962  df-if 4461

This theorem is referenced by:  csbif  4515  nfop  4812  nfrdg  8043  boxcutc  8498  nfoi  8971  nfsum1  15041  nfsumw  15042  nfsum  15043  summolem2a  15067  zsum  15070  sumss  15076  sumss2  15078  fsumcvg2  15079  nfcprod  15260  cbvprod  15264  prodmolem2a  15283  zprod  15286  fprod  15290  fprodntriv  15291  prodss  15296  pcmpt  16223  pcmptdvds  16225  gsummpt1n0  19080  madugsum  21247  mbfpos  24247  mbfposb  24249  i1fposd  24303  isibl2  24362  nfitg  24370  cbvitg  24371  itgss3  24410  itgcn  24440  limcmpt  24478  rlimcnp2  25542  chirred  30170  nosupbnd2  33237  cdleme31sn  37549  cdleme32d  37613  cdleme32f  37615  refsum2cn  41369  ssfiunibd  41650  uzub  41779  limsupubuz  42068  icccncfext  42244  fourierdlem86  42551  vonicc  43041  nfafv  43409  nfafv2  43491