Theorem nfif 4486

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

Syntax hints:  ⊤wtru 1540  Ⅎwnf 1787  Ⅎwnfc 2886  ifcif 4456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-if 4457

This theorem is referenced by:  csbif  4513  nfop  4817  nfrdg  8216  boxcutc  8687  nfoi  9203  nfsum1  15329  nfsum  15330  nfsumOLD  15331  summolem2a  15355  zsum  15358  sumss  15364  sumss2  15366  fsumcvg2  15367  nfcprod  15549  cbvprod  15553  prodmolem2a  15572  zprod  15575  fprod  15579  fprodntriv  15580  prodss  15585  pcmpt  16521  pcmptdvds  16523  gsummpt1n0  19481  madugsum  21700  mbfpos  24720  mbfposb  24722  i1fposd  24777  isibl2  24836  nfitg  24844  cbvitg  24845  itgss3  24884  itgcn  24914  limcmpt  24952  rlimcnp2  26021  chirred  30658  nosupbnd2  33846  noinfbnd2  33861  cdleme31sn  38321  cdleme32d  38385  cdleme32f  38387  refsum2cn  42470  ssfiunibd  42738  uzub  42861  limsupubuz  43144  icccncfext  43318  fourierdlem86  43623  vonicc  44113  nfafv  44515  nfafv2  44597