Theorem nfif 4503

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

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

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 4473

This theorem is referenced by:  csbif  4530  nfop  4838  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  19877  madugsum  22558  mbfpos  25579  mbfposb  25581  i1fposd  25635  isibl2  25694  nfitg  25703  cbvitg  25704  itgss3  25743  itgcn  25773  limcmpt  25811  rlimcnp2  26903  nosupbnd2  27655  noinfbnd2  27670  chirred  32375  cdleme31sn  40489  cdleme32d  40553  cdleme32f  40555  refsum2cn  45145  ssfiunibd  45420  uzub  45539  limsupubuz  45821  icccncfext  45995  fourierdlem86  46300  vonicc  46793  nfafv  47246  nfafv2  47328