Theorem nfif 4558

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

Syntax hints:  ⊤wtru 1542  Ⅎwnf 1785  Ⅎwnfc 2883  ifcif 4528

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-if 4529

This theorem is referenced by:  csbif  4585  nfop  4889  nfrdg  8413  boxcutc  8934  nfoi  9508  nfsum1  15635  nfsum  15636  summolem2a  15660  zsum  15663  sumss  15669  sumss2  15671  fsumcvg2  15672  nfcprod  15854  cbvprod  15858  prodmolem2a  15877  zprod  15880  fprod  15884  fprodntriv  15885  prodss  15890  pcmpt  16824  pcmptdvds  16826  gsummpt1n0  19832  madugsum  22144  mbfpos  25167  mbfposb  25169  i1fposd  25224  isibl2  25283  nfitg  25291  cbvitg  25292  itgss3  25331  itgcn  25361  limcmpt  25399  rlimcnp2  26468  nosupbnd2  27216  noinfbnd2  27231  chirred  31643  cdleme31sn  39246  cdleme32d  39310  cdleme32f  39312  refsum2cn  43712  ssfiunibd  44009  uzub  44131  limsupubuz  44419  icccncfext  44593  fourierdlem86  44898  vonicc  45391  nfafv  45834  nfafv2  45916