Theorem nfif 4498

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

Syntax hints:  ⊤wtru 1543  Ⅎwnf 1785  Ⅎwnfc 2884  ifcif 4467

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-if 4468

This theorem is referenced by:  csbif  4525  nfop  4833  nfrdg  8346  boxcutc  8882  nfoi  9422  nfsum1  15643  nfsum  15644  summolem2a  15668  zsum  15671  sumss  15677  sumss2  15679  fsumcvg2  15680  nfcprod  15865  cbvprod  15869  prodmolem2a  15890  zprod  15893  fprod  15897  fprodntriv  15898  prodss  15903  pcmpt  16854  pcmptdvds  16856  gsummpt1n0  19931  madugsum  22618  mbfpos  25628  mbfposb  25630  i1fposd  25684  isibl2  25743  nfitg  25752  cbvitg  25753  itgss3  25792  itgcn  25822  limcmpt  25860  rlimcnp2  26943  nosupbnd2  27694  noinfbnd2  27709  chirred  32481  cdleme31sn  40840  cdleme32d  40904  cdleme32f  40906  refsum2cn  45487  ssfiunibd  45760  uzub  45877  limsupubuz  46159  icccncfext  46333  fourierdlem86  46638  vonicc  47131  nfafv  47596  nfafv2  47678