Theorem nfif 4512

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

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

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 4482

This theorem is referenced by:  csbif  4539  nfop  4847  nfrdg  8355  boxcutc  8891  nfoi  9431  nfsum1  15625  nfsum  15626  summolem2a  15650  zsum  15653  sumss  15659  sumss2  15661  fsumcvg2  15662  nfcprod  15844  cbvprod  15848  prodmolem2a  15869  zprod  15872  fprod  15876  fprodntriv  15877  prodss  15882  pcmpt  16832  pcmptdvds  16834  gsummpt1n0  19906  madugsum  22599  mbfpos  25620  mbfposb  25622  i1fposd  25676  isibl2  25735  nfitg  25744  cbvitg  25745  itgss3  25784  itgcn  25814  limcmpt  25852  rlimcnp2  26944  nosupbnd2  27696  noinfbnd2  27711  chirred  32482  cdleme31sn  40753  cdleme32d  40817  cdleme32f  40819  refsum2cn  45395  ssfiunibd  45668  uzub  45786  limsupubuz  46068  icccncfext  46242  fourierdlem86  46547  vonicc  47040  nfafv  47493  nfafv2  47575