Theorem nfif 4522

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

Syntax hints:  ⊤wtru 1541  Ⅎwnf 1783  Ⅎwnfc 2877  ifcif 4491

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 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-if 4492

This theorem is referenced by:  csbif  4549  nfop  4856  nfrdg  8385  boxcutc  8917  nfoi  9474  nfsum1  15663  nfsum  15664  summolem2a  15688  zsum  15691  sumss  15697  sumss2  15699  fsumcvg2  15700  nfcprod  15882  cbvprod  15886  prodmolem2a  15907  zprod  15910  fprod  15914  fprodntriv  15915  prodss  15920  pcmpt  16870  pcmptdvds  16872  gsummpt1n0  19902  madugsum  22537  mbfpos  25559  mbfposb  25561  i1fposd  25615  isibl2  25674  nfitg  25683  cbvitg  25684  itgss3  25723  itgcn  25753  limcmpt  25791  rlimcnp2  26883  nosupbnd2  27635  noinfbnd2  27650  chirred  32331  cdleme31sn  40381  cdleme32d  40445  cdleme32f  40447  refsum2cn  45039  ssfiunibd  45314  uzub  45434  limsupubuz  45718  icccncfext  45892  fourierdlem86  46197  vonicc  46690  nfafv  47141  nfafv2  47223