Theorem nfif 4519

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

Syntax hints:  ⊤wtru 1571  Ⅎwnf 1813  Ⅎwnfc 2910  ifcif 4488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-nf 1814  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-if 4489

This theorem is referenced by:  csbif  4546  nfop  4855  nfrdg  8402  boxcutc  8940  nfoi  9477  nfsum1  15743  nfsum  15744  summolem2a  15768  zsum  15771  sumss  15777  sumss2  15779  fsumcvg2  15780  nfcprod  15965  cbvprod  15969  prodmolem2a  15990  zprod  15993  fprod  15997  fprodntriv  15998  prodss  16003  pcmpt  16953  pcmptdvds  16955  gsummpt1n0  20036  madugsum  22781  mbfpos  25791  mbfposb  25793  i1fposd  25847  isibl2  25906  nfitg  25915  cbvitg  25916  itgss3  25955  itgcn  25985  limcmpt  26023  rlimcnp2  27112  nosupbnd2  27861  noinfbnd2  27876  chirred  32728  cdleme31sn  41135  cdleme32d  41199  cdleme32f  41201  refsum2cn  45741  ssfiunibd  46011  uzub  46128  limsupubuz  46410  icccncfext  46584  fourierdlem86  46889  vonicc  47382  nfafv  47856  nfafv2  47938