Theorem nfif 4410

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

Syntax hints:  ⊤wtru 1523  Ⅎwnf 1765  Ⅎwnfc 2933  ifcif 4381

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-if 4382

This theorem is referenced by:  csbif  4436  nfop  4726  nfrdg  7902  boxcutc  8353  nfoi  8824  nfsum1  14880  nfsum  14881  summolem2a  14905  zsum  14908  sumss  14914  sumss2  14916  fsumcvg2  14917  nfcprod  15098  cbvprod  15102  prodmolem2a  15121  zprod  15124  fprod  15128  fprodntriv  15129  prodss  15134  pcmpt  16057  pcmptdvds  16059  gsummpt1n0  18805  madugsum  20936  mbfpos  23935  mbfposb  23937  i1fposd  23991  isibl2  24050  nfitg  24058  cbvitg  24059  itgss3  24098  itgcn  24126  limcmpt  24164  rlimcnp2  25226  chirred  29863  nosupbnd2  32825  cdleme31sn  37047  cdleme32d  37111  cdleme32f  37113  refsum2cn  40834  ssfiunibd  41117  uzub  41247  limsupubuz  41536  icccncfext  41711  fourierdlem86  42019  vonicc  42509  nfafv  42851  nfafv2  42933