Theorem nfif 4492

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

Syntax hints:  ⊤wtru 1548  Ⅎwnf 1790  Ⅎwnfc 2887  ifcif 4461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-if 4462

This theorem is referenced by:  csbif  4519  nfop  4827  nfrdg  8350  boxcutc  8886  nfoi  9426  nfsum1  15650  nfsum  15651  summolem2a  15675  zsum  15678  sumss  15684  sumss2  15686  fsumcvg2  15687  nfcprod  15872  cbvprod  15876  prodmolem2a  15897  zprod  15900  fprod  15904  fprodntriv  15905  prodss  15910  pcmpt  16861  pcmptdvds  16863  gsummpt1n0  19938  madugsum  22633  mbfpos  25643  mbfposb  25645  i1fposd  25699  isibl2  25758  nfitg  25767  cbvitg  25768  itgss3  25807  itgcn  25837  limcmpt  25875  rlimcnp2  26955  nosupbnd2  27705  noinfbnd2  27720  chirred  32491  cdleme31sn  40879  cdleme32d  40943  cdleme32f  40945  refsum2cn  45493  ssfiunibd  45764  uzub  45881  limsupubuz  46163  icccncfext  46337  fourierdlem86  46642  vonicc  47135  nfafv  47606  nfafv2  47688