Theorem nfif 4508

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

Syntax hints:  ⊤wtru 1560  Ⅎwnf 1802  Ⅎwnfc 2908  ifcif 4477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-nf 1803  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-if 4478

This theorem is referenced by:  csbif  4535  nfop  4844  nfrdg  8378  boxcutc  8916  nfoi  9455  nfsum1  15707  nfsum  15708  summolem2a  15732  zsum  15735  sumss  15741  sumss2  15743  fsumcvg2  15744  nfcprod  15929  cbvprod  15933  prodmolem2a  15954  zprod  15957  fprod  15961  fprodntriv  15962  prodss  15967  pcmpt  16918  pcmptdvds  16920  gsummpt1n0  19995  madugsum  22690  mbfpos  25700  mbfposb  25702  i1fposd  25756  isibl2  25815  nfitg  25824  cbvitg  25825  itgss3  25864  itgcn  25894  limcmpt  25932  rlimcnp2  27018  nosupbnd2  27767  noinfbnd2  27782  chirred  32554  cdleme31sn  40964  cdleme32d  41028  cdleme32f  41030  refsum2cn  45578  ssfiunibd  45848  uzub  45965  limsupubuz  46247  icccncfext  46421  fourierdlem86  46726  vonicc  47219  nfafv  47690  nfafv2  47772