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

Theorem elvd 3439
Description: If a proposition is implied by 𝑥 ∈ V (which is true, see vex 3437) and another antecedent, then it is implied by that other antecedent. Deduction associated with elv 3438. (Contributed by Peter Mazsa, 23-Oct-2018.)
Hypothesis
Ref Expression
elvd.1 ((𝜑𝑥 ∈ V) → 𝜓)
Assertion
Ref Expression
elvd (𝜑𝜓)

Proof of Theorem elvd
StepHypRef Expression
1 vex 3437 . 2 𝑥 ∈ V
2 elvd.1 . 2 ((𝜑𝑥 ∈ V) → 𝜓)
31, 2mpan2 691 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wcel 2109  Vcvv 3433
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-ext 2701
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3435
This theorem is referenced by:  inimasn  6099  predep  6272  dffv3  6812  dmfco  6912  fsnex  7211  2ndconst  8025  curry1  8028  qsel  8714  ralxpmap  8814  domunsn  9034  dif1ennnALT  9155  eqinf  9363  dfacacn  10024  dfac13  10025  intgru  10696  shftfib  14966  rlimdm  15445  mat1scmat  22408  imasnopn  23559  imasncld  23560  imasncls  23561  ustuqtop1  24110  ustuqtop2  24111  ustuqtop3  24112  blval2  24431  mulsval  28002  dfnbgr2  29269  nbuhgr  29275  iunsnima2  32554  gblacfnacd  35092  vonf1owev  35098  fmlasucdisj  35389  opelco3  35765  funpartfv  35936  tailfb  36368  el3v23  38219  eldm4  38266  eldmcnv  38330  ecin0  38337  brcoss3  38427  refressn  38437  disjlem19  38796  pwslnmlem1  43082  rlimdmafv  47175  dfatsnafv2  47250  dfafv23  47251  dfatdmfcoafv2  47252  rlimdmafv2  47256  dfclnbgr2  47821  uspgrsprfo  48146
  Copyright terms: Public domain W3C validator