Theorem nfif 4516

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

This proof depends on syntax axioms:  ⊤wtru 1571  Ⅎwnf 1816  Ⅎwnfc 2911  ifcif 4485

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-if 4486

This theorem is used by:  csbif  4543  nfop  4854  nfrdg  8460  boxcutc  9007  nfoi  9545  nfsum1  15901  nfsum  15902  summolem2a  15925  zsum  15928  sumss  15934  sumss2  15936  fsumcvg2  15937  nfcprod  16122  cbvprod  16126  prodmolem2a  16145  zprod  16148  fprod  16152  fprodntriv  16153  prodss  16158  pcmpt  17114  pcmptdvds  17116  gsummpt1n0  20230  madugsum  23013  mbfpos  26027  mbfposb  26029  i1fposd  26083  isibl2  26142  nfitg  26150  cbvitg  26151  itgss3  26190  itgcn  26220  limcmpt  26258  rlimcnp2  27351  nosupbnd2  28130  noinfbnd2  28145  chirred  33054  cdleme31sn  41703  cdleme32d  41767  cdleme32f  41769  refsum2cn  46329  ssfiunibd  46598  uzub  46714  limsupubuz  46996  icccncfext  47170  fourierdlem86  47475  vonicc  47968  nfafv  48479  nfafv2  48561