Theorem nfif 4559

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

Syntax hints:  ⊤wtru 1543  Ⅎwnf 1786  Ⅎwnfc 2884  ifcif 4529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-if 4530

This theorem is referenced by:  csbif  4586  nfop  4890  nfrdg  8414  boxcutc  8935  nfoi  9509  nfsum1  15636  nfsum  15637  summolem2a  15661  zsum  15664  sumss  15670  sumss2  15672  fsumcvg2  15673  nfcprod  15855  cbvprod  15859  prodmolem2a  15878  zprod  15881  fprod  15885  fprodntriv  15886  prodss  15891  pcmpt  16825  pcmptdvds  16827  gsummpt1n0  19833  madugsum  22145  mbfpos  25168  mbfposb  25170  i1fposd  25225  isibl2  25284  nfitg  25292  cbvitg  25293  itgss3  25332  itgcn  25362  limcmpt  25400  rlimcnp2  26471  nosupbnd2  27219  noinfbnd2  27234  chirred  31648  cdleme31sn  39251  cdleme32d  39315  cdleme32f  39317  refsum2cn  43722  ssfiunibd  44019  uzub  44141  limsupubuz  44429  icccncfext  44603  fourierdlem86  44908  vonicc  45401  nfafv  45844  nfafv2  45926