Theorem nfif 4455

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

Syntax hints:  ⊤wtru 1544  Ⅎwnf 1791  Ⅎwnfc 2877  ifcif 4425

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-nf 1792  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-if 4426

This theorem is referenced by:  csbif  4482  nfop  4786  nfrdg  8128  boxcutc  8600  nfoi  9108  nfsum1  15218  nfsum  15219  nfsumOLD  15220  summolem2a  15244  zsum  15247  sumss  15253  sumss2  15255  fsumcvg2  15256  nfcprod  15436  cbvprod  15440  prodmolem2a  15459  zprod  15462  fprod  15466  fprodntriv  15467  prodss  15472  pcmpt  16408  pcmptdvds  16410  gsummpt1n0  19304  madugsum  21494  mbfpos  24502  mbfposb  24504  i1fposd  24559  isibl2  24618  nfitg  24626  cbvitg  24627  itgss3  24666  itgcn  24696  limcmpt  24734  rlimcnp2  25803  chirred  30430  nosupbnd2  33605  noinfbnd2  33620  cdleme31sn  38080  cdleme32d  38144  cdleme32f  38146  refsum2cn  42195  ssfiunibd  42462  uzub  42585  limsupubuz  42872  icccncfext  43046  fourierdlem86  43351  vonicc  43841  nfafv  44243  nfafv2  44325