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

Theorem elvd 3391
Description: If a proposition is implied by 𝑥 ∈ V (which is true, see vex 3389) and another antecedent, then it is implied by that other antecedent. Deduction associated with elv 3390. (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 3389 . 2 𝑥 ∈ V
2 elvd.1 . 2 ((𝜑𝑥 ∈ V) → 𝜓)
31, 2mpan2 683 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385  wcel 2157  Vcvv 3386
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-12 2213  ax-ext 2778
This theorem depends on definitions:  df-bi 199  df-an 386  df-tru 1657  df-ex 1876  df-sb 2065  df-clab 2787  df-cleq 2793  df-clel 2796  df-v 3388
This theorem is referenced by:  inimasn  5768  predep  5925  dffv3  6408  dmfco  6498  fsnex  6767  2ndconst  7504  curry1  7507  qsel  8065  ralxpmap  8148  domunsn  8353  dif1en  8436  eqinf  8633  dfacacn  9252  dfac13  9253  intgru  9925  shftfib  14152  rlimdm  14622  mat1scmat  20670  imasnopn  21821  imasncld  21822  imasncls  21823  ustuqtop1  22372  ustuqtop2  22373  ustuqtop3  22374  blval2  22694  dfnbgr2  26571  nbuhgr  26580  opelco3  32189  funpartfv  32564  tailfb  32883  el3v23  34498  eldm4  34533  eldmcnv  34606  ecin0  34610  brcoss3  34681  pwslnmlem1  38442  rlimdmafv  42026  dfatsnafv2  42101  dfafv23  42102  dfatdmfcoafv2  42103  rlimdmafv2  42107  uspgrsprfo  42550
  Copyright terms: Public domain W3C validator