Theorem nfif 4507

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

Syntax hints:  ⊤wtru 1542  Ⅎwnf 1784  Ⅎwnfc 2880  ifcif 4476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-if 4477

This theorem is referenced by:  csbif  4534  nfop  4842  nfrdg  8341  boxcutc  8873  nfoi  9409  nfsum1  15601  nfsum  15602  summolem2a  15626  zsum  15629  sumss  15635  sumss2  15637  fsumcvg2  15638  nfcprod  15820  cbvprod  15824  prodmolem2a  15845  zprod  15848  fprod  15852  fprodntriv  15853  prodss  15858  pcmpt  16808  pcmptdvds  16810  gsummpt1n0  19881  madugsum  22561  mbfpos  25582  mbfposb  25584  i1fposd  25638  isibl2  25697  nfitg  25706  cbvitg  25707  itgss3  25746  itgcn  25776  limcmpt  25814  rlimcnp2  26906  nosupbnd2  27658  noinfbnd2  27673  chirred  32379  cdleme31sn  40502  cdleme32d  40566  cdleme32f  40568  refsum2cn  45162  ssfiunibd  45437  uzub  45556  limsupubuz  45838  icccncfext  46012  fourierdlem86  46317  vonicc  46810  nfafv  47263  nfafv2  47345