Theorem nfif 4506

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

Syntax hints:  ⊤wtru 1542  Ⅎwnf 1784  Ⅎwnfc 2879  ifcif 4475

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 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-if 4476

This theorem is referenced by:  csbif  4533  nfop  4841  nfrdg  8333  boxcutc  8865  nfoi  9400  nfsum1  15597  nfsum  15598  summolem2a  15622  zsum  15625  sumss  15631  sumss2  15633  fsumcvg2  15634  nfcprod  15816  cbvprod  15820  prodmolem2a  15841  zprod  15844  fprod  15848  fprodntriv  15849  prodss  15854  pcmpt  16804  pcmptdvds  16806  gsummpt1n0  19878  madugsum  22559  mbfpos  25580  mbfposb  25582  i1fposd  25636  isibl2  25695  nfitg  25704  cbvitg  25705  itgss3  25744  itgcn  25774  limcmpt  25812  rlimcnp2  26904  nosupbnd2  27656  noinfbnd2  27671  chirred  32373  cdleme31sn  40425  cdleme32d  40489  cdleme32f  40491  refsum2cn  45081  ssfiunibd  45356  uzub  45475  limsupubuz  45757  icccncfext  45931  fourierdlem86  46236  vonicc  46729  nfafv  47173  nfafv2  47255