Theorem nfif 4510

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

Syntax hints:  ⊤wtru 1542  Ⅎwnf 1784  Ⅎwnfc 2883  ifcif 4479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-if 4480

This theorem is referenced by:  csbif  4537  nfop  4845  nfrdg  8345  boxcutc  8879  nfoi  9419  nfsum1  15613  nfsum  15614  summolem2a  15638  zsum  15641  sumss  15647  sumss2  15649  fsumcvg2  15650  nfcprod  15832  cbvprod  15836  prodmolem2a  15857  zprod  15860  fprod  15864  fprodntriv  15865  prodss  15870  pcmpt  16820  pcmptdvds  16822  gsummpt1n0  19894  madugsum  22587  mbfpos  25608  mbfposb  25610  i1fposd  25664  isibl2  25723  nfitg  25732  cbvitg  25733  itgss3  25772  itgcn  25802  limcmpt  25840  rlimcnp2  26932  nosupbnd2  27684  noinfbnd2  27699  chirred  32470  cdleme31sn  40640  cdleme32d  40704  cdleme32f  40706  refsum2cn  45283  ssfiunibd  45557  uzub  45675  limsupubuz  45957  icccncfext  46131  fourierdlem86  46436  vonicc  46929  nfafv  47382  nfafv2  47464