Theorem nfif 4148

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

Syntax hints:  ⊤wtru 1524  Ⅎwnf 1748  Ⅎwnfc 2780  ifcif 4119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-if 4120

This theorem is referenced by:  csbif  4171  nfop  4449  nfrdg  7555  boxcutc  7993  nfoi  8460  nfsum1  14464  nfsum  14465  summolem2a  14490  zsum  14493  sumss  14499  sumss2  14501  fsumcvg2  14502  nfcprod  14685  cbvprod  14689  prodmolem2a  14708  zprod  14711  fprod  14715  fprodntriv  14716  prodss  14721  pcmpt  15643  pcmptdvds  15645  gsummpt1n0  18410  madugsum  20497  mbfpos  23463  mbfposb  23465  i1fposd  23519  isibl2  23578  nfitg  23586  cbvitg  23587  itgss3  23626  itgcn  23654  limcmpt  23692  rlimcnp2  24738  chirred  29382  nosupbnd2  31987  cdleme31sn  35985  cdleme32d  36049  cdleme32f  36051  refsum2cn  39511  ssfiunibd  39837  uzub  39971  limsupubuz  40263  icccncfext  40418  fourierdlem86  40727  vonicc  41220  nfafv  41537