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

Theorem elvd 3468
Description: If a proposition is implied by 𝑥 ∈ V (which is true, see vex 3465) and another antecedent, then it is implied by that other antecedent. Deduction associated with elv 3467. (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 3465 . 2 𝑥 ∈ V
2 elvd.1 . 2 ((𝜑𝑥 ∈ V) → 𝜓)
31, 2mpan2 689 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  wcel 2098  Vcvv 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-v 3463
This theorem is referenced by:  inimasn  6162  predep  6338  dffv3  6892  dmfco  6993  fsnex  7292  2ndconst  8106  curry1  8109  qsel  8815  ralxpmap  8915  domunsn  9152  dif1ennnALT  9302  eqinf  9509  dfacacn  10166  dfac13  10167  intgru  10839  shftfib  15055  rlimdm  15531  mat1scmat  22485  imasnopn  23638  imasncld  23639  imasncls  23640  ustuqtop1  24190  ustuqtop2  24191  ustuqtop3  24192  blval2  24515  mulsval  28059  dfnbgr2  29222  nbuhgr  29228  iunsnima2  32488  fmlasucdisj  35140  opelco3  35501  funpartfv  35672  tailfb  35992  el3v23  37828  eldm4  37876  eldmcnv  37947  ecin0  37954  brcoss3  38035  refressn  38045  disjlem19  38403  pwslnmlem1  42658  rlimdmafv  46695  dfatsnafv2  46770  dfafv23  46771  dfatdmfcoafv2  46772  rlimdmafv2  46776  dfclnbgr2  47300  uspgrsprfo  47396
  Copyright terms: Public domain W3C validator