Theorem nfif 4512

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

This proof depends on syntax axioms:  ⊤wtru 1570  Ⅎwnf 1815  Ⅎwnfc 2907  ifcif 4481

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-if 4482

This theorem is used by:  csbif  4539  nfop  4848  nfrdg  8426  boxcutc  8973  nfoi  9512  nfsum1  15863  nfsum  15864  summolem2a  15887  zsum  15890  sumss  15896  sumss2  15898  fsumcvg2  15899  nfcprod  16084  cbvprod  16088  prodmolem2a  16107  zprod  16110  fprod  16114  fprodntriv  16115  prodss  16120  pcmpt  17076  pcmptdvds  17078  gsummpt1n0  20185  madugsum  22964  mbfpos  25978  mbfposb  25980  i1fposd  26034  isibl2  26093  nfitg  26101  cbvitg  26102  itgss3  26141  itgcn  26171  limcmpt  26209  rlimcnp2  27300  nosupbnd2  28079  noinfbnd2  28094  chirred  33003  cdleme31sn  41531  cdleme32d  41595  cdleme32f  41597  refsum2cn  46149  ssfiunibd  46419  uzub  46535  limsupubuz  46817  icccncfext  46991  fourierdlem86  47296  vonicc  47789  nfafv  48300  nfafv2  48382