MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfif Structured version   Visualization version   GIF version

Theorem nfif 4148
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
StepHypRef Expression
1 nfif.1 . . . 4 𝑥𝜑
21a1i 11 . . 3 (⊤ → Ⅎ𝑥𝜑)
3 nfif.2 . . . 4 𝑥𝐴
43a1i 11 . . 3 (⊤ → 𝑥𝐴)
5 nfif.3 . . . 4 𝑥𝐵
65a1i 11 . . 3 (⊤ → 𝑥𝐵)
72, 4, 6nfifd 4147 . 2 (⊤ → 𝑥if(𝜑, 𝐴, 𝐵))
87trud 1533 1 𝑥if(𝜑, 𝐴, 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wtru 1524  wnf 1748  wnfc 2780  ifcif 4119
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-if 4120
This theorem is referenced by:  csbif  4171  nfop  4449  nfrdg  7555  boxcutc  7993  nfoi  8460  nfsum1  14464  nfsum  14465  summolem2a  14490  zsum  14493  sumss  14499  sumss2  14501  fsumcvg2  14502  nfcprod  14685  cbvprod  14689  prodmolem2a  14708  zprod  14711  fprod  14715  fprodntriv  14716  prodss  14721  pcmpt  15643  pcmptdvds  15645  gsummpt1n0  18410  madugsum  20497  mbfpos  23463  mbfposb  23465  i1fposd  23519  isibl2  23578  nfitg  23586  cbvitg  23587  itgss3  23626  itgcn  23654  limcmpt  23692  rlimcnp2  24738  chirred  29382  nosupbnd2  31987  cdleme31sn  35985  cdleme32d  36049  cdleme32f  36051  refsum2cn  39511  ssfiunibd  39837  uzub  39971  limsupubuz  40263  icccncfext  40418  fourierdlem86  40727  vonicc  41220  nfafv  41537
  Copyright terms: Public domain W3C validator