Theorem nfif 4489

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

Syntax hints:  ⊤wtru 1540  Ⅎwnf 1786  Ⅎwnfc 2887  ifcif 4459

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-if 4460

This theorem is referenced by:  csbif  4516  nfop  4820  nfrdg  8245  boxcutc  8729  nfoi  9273  nfsum1  15401  nfsum  15402  nfsumOLD  15403  summolem2a  15427  zsum  15430  sumss  15436  sumss2  15438  fsumcvg2  15439  nfcprod  15621  cbvprod  15625  prodmolem2a  15644  zprod  15647  fprod  15651  fprodntriv  15652  prodss  15657  pcmpt  16593  pcmptdvds  16595  gsummpt1n0  19566  madugsum  21792  mbfpos  24815  mbfposb  24817  i1fposd  24872  isibl2  24931  nfitg  24939  cbvitg  24940  itgss3  24979  itgcn  25009  limcmpt  25047  rlimcnp2  26116  chirred  30757  nosupbnd2  33919  noinfbnd2  33934  cdleme31sn  38394  cdleme32d  38458  cdleme32f  38460  refsum2cn  42581  ssfiunibd  42848  uzub  42971  limsupubuz  43254  icccncfext  43428  fourierdlem86  43733  vonicc  44223  nfafv  44628  nfafv2  44710