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

Theorem nfif 4254
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 4253 . 2 (⊤ → 𝑥if(𝜑, 𝐴, 𝐵))
87trud 1641 1 𝑥if(𝜑, 𝐴, 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wtru 1632  wnf 1856  wnfc 2900  ifcif 4225
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-if 4226
This theorem is referenced by:  csbif  4277  nfop  4555  nfrdg  7663  boxcutc  8105  nfoi  8575  nfsum1  14628  nfsum  14629  summolem2a  14654  zsum  14657  sumss  14663  sumss2  14665  fsumcvg2  14666  nfcprod  14848  cbvprod  14852  prodmolem2a  14871  zprod  14874  fprod  14878  fprodntriv  14879  prodss  14884  pcmpt  15803  pcmptdvds  15805  gsummpt1n0  18571  madugsum  20667  mbfpos  23638  mbfposb  23640  i1fposd  23694  isibl2  23753  nfitg  23761  cbvitg  23762  itgss3  23801  itgcn  23829  limcmpt  23867  rlimcnp2  24914  chirred  29594  nosupbnd2  32199  cdleme31sn  36189  cdleme32d  36253  cdleme32f  36255  refsum2cn  39719  ssfiunibd  40040  uzub  40174  limsupubuz  40463  icccncfext  40618  fourierdlem86  40926  vonicc  41419  nfafv  41736
  Copyright terms: Public domain W3C validator