Theorem nfif 4578

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

Syntax hints:  ⊤wtru 1538  Ⅎwnf 1781  Ⅎwnfc 2893  ifcif 4548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-nf 1782  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-if 4549

This theorem is referenced by:  csbif  4605  nfop  4913  nfrdg  8470  boxcutc  8999  nfoi  9583  nfsum1  15738  nfsum  15739  summolem2a  15763  zsum  15766  sumss  15772  sumss2  15774  fsumcvg2  15775  nfcprod  15957  cbvprod  15961  prodmolem2a  15982  zprod  15985  fprod  15989  fprodntriv  15990  prodss  15995  pcmpt  16939  pcmptdvds  16941  gsummpt1n0  20007  madugsum  22670  mbfpos  25705  mbfposb  25707  i1fposd  25762  isibl2  25821  nfitg  25830  cbvitg  25831  itgss3  25870  itgcn  25900  limcmpt  25938  rlimcnp2  27027  nosupbnd2  27779  noinfbnd2  27794  chirred  32427  cdleme31sn  40337  cdleme32d  40401  cdleme32f  40403  refsum2cn  44938  ssfiunibd  45224  uzub  45346  limsupubuz  45634  icccncfext  45808  fourierdlem86  46113  vonicc  46606  nfafv  47051  nfafv2  47133