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

Theorem nfif 4457
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 4456 . 2 (⊤ → 𝑥if(𝜑, 𝐴, 𝐵))
87mptru 1545 1 𝑥if(𝜑, 𝐴, 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wtru 1539  wnf 1785  wnfc 2939  ifcif 4428
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-if 4429
This theorem is referenced by:  csbif  4483  nfop  4784  nfrdg  8037  boxcutc  8492  nfoi  8966  nfsum1  15041  nfsum  15042  nfsumOLD  15043  summolem2a  15067  zsum  15070  sumss  15076  sumss2  15078  fsumcvg2  15079  nfcprod  15260  cbvprod  15264  prodmolem2a  15283  zprod  15286  fprod  15290  fprodntriv  15291  prodss  15296  pcmpt  16221  pcmptdvds  16223  gsummpt1n0  19081  madugsum  21251  mbfpos  24258  mbfposb  24260  i1fposd  24314  isibl2  24373  nfitg  24381  cbvitg  24382  itgss3  24421  itgcn  24451  limcmpt  24489  rlimcnp2  25555  chirred  30181  nosupbnd2  33324  cdleme31sn  37669  cdleme32d  37733  cdleme32f  37735  refsum2cn  41654  ssfiunibd  41928  uzub  42055  limsupubuz  42342  icccncfext  42516  fourierdlem86  42821  vonicc  43311  nfafv  43679  nfafv2  43761
  Copyright terms: Public domain W3C validator