Theorem nfif 4561

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

Syntax hints:  ⊤wtru 1538  Ⅎwnf 1780  Ⅎwnfc 2888  ifcif 4531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-nf 1781  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-if 4532

This theorem is referenced by:  csbif  4588  nfop  4894  nfrdg  8453  boxcutc  8980  nfoi  9552  nfsum1  15723  nfsum  15724  summolem2a  15748  zsum  15751  sumss  15757  sumss2  15759  fsumcvg2  15760  nfcprod  15942  cbvprod  15946  prodmolem2a  15967  zprod  15970  fprod  15974  fprodntriv  15975  prodss  15980  pcmpt  16926  pcmptdvds  16928  gsummpt1n0  19998  madugsum  22665  mbfpos  25700  mbfposb  25702  i1fposd  25757  isibl2  25816  nfitg  25825  cbvitg  25826  itgss3  25865  itgcn  25895  limcmpt  25933  rlimcnp2  27024  nosupbnd2  27776  noinfbnd2  27791  chirred  32424  cdleme31sn  40363  cdleme32d  40427  cdleme32f  40429  refsum2cn  44976  ssfiunibd  45260  uzub  45381  limsupubuz  45669  icccncfext  45843  fourierdlem86  46148  vonicc  46641  nfafv  47086  nfafv2  47168