Theorem nfif 4519

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

Syntax hints:  ⊤wtru 1541  Ⅎwnf 1783  Ⅎwnfc 2876  ifcif 4488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-if 4489

This theorem is referenced by:  csbif  4546  nfop  4853  nfrdg  8382  boxcutc  8914  nfoi  9467  nfsum1  15656  nfsum  15657  summolem2a  15681  zsum  15684  sumss  15690  sumss2  15692  fsumcvg2  15693  nfcprod  15875  cbvprod  15879  prodmolem2a  15900  zprod  15903  fprod  15907  fprodntriv  15908  prodss  15913  pcmpt  16863  pcmptdvds  16865  gsummpt1n0  19895  madugsum  22530  mbfpos  25552  mbfposb  25554  i1fposd  25608  isibl2  25667  nfitg  25676  cbvitg  25677  itgss3  25716  itgcn  25746  limcmpt  25784  rlimcnp2  26876  nosupbnd2  27628  noinfbnd2  27643  chirred  32324  cdleme31sn  40374  cdleme32d  40438  cdleme32f  40440  refsum2cn  45032  ssfiunibd  45307  uzub  45427  limsupubuz  45711  icccncfext  45885  fourierdlem86  46190  vonicc  46683  nfafv  47137  nfafv2  47219