Theorem nfif 4498

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

Syntax hints:  ⊤wtru 1538  Ⅎwnf 1784  Ⅎwnfc 2963  ifcif 4469

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-if 4470

This theorem is referenced by:  csbif  4524  nfop  4821  nfrdg  8052  boxcutc  8507  nfoi  8980  nfsum1  15048  nfsumw  15049  nfsum  15050  summolem2a  15074  zsum  15077  sumss  15083  sumss2  15085  fsumcvg2  15086  nfcprod  15267  cbvprod  15271  prodmolem2a  15290  zprod  15293  fprod  15297  fprodntriv  15298  prodss  15303  pcmpt  16230  pcmptdvds  16232  gsummpt1n0  19087  madugsum  21254  mbfpos  24254  mbfposb  24256  i1fposd  24310  isibl2  24369  nfitg  24377  cbvitg  24378  itgss3  24417  itgcn  24445  limcmpt  24483  rlimcnp2  25546  chirred  30174  nosupbnd2  33218  cdleme31sn  37518  cdleme32d  37582  cdleme32f  37584  refsum2cn  41302  ssfiunibd  41583  uzub  41712  limsupubuz  42001  icccncfext  42177  fourierdlem86  42484  vonicc  42974  nfafv  43342  nfafv2  43424