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

Theorem elvd 3451
Description: If a proposition is implied by 𝑥 ∈ V (which is true, see vex 3448) and another antecedent, then it is implied by that other antecedent. Deduction associated with elv 3450. (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 3448 . 2 𝑥 ∈ V
2 elvd.1 . 2 ((𝜑𝑥 ∈ V) → 𝜓)
31, 2mpan2 690 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wcel 2107  Vcvv 3444
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3446
This theorem is referenced by:  inimasn  6107  predep  6283  dffv3  6836  dmfco  6935  fsnex  7226  2ndconst  8026  curry1  8029  qsel  8694  ralxpmap  8793  domunsn  9030  dif1ennnALT  9180  eqinf  9379  dfacacn  10036  dfac13  10037  intgru  10709  shftfib  14917  rlimdm  15393  mat1scmat  21840  imasnopn  22993  imasncld  22994  imasncls  22995  ustuqtop1  23545  ustuqtop2  23546  ustuqtop3  23547  blval2  23870  dfnbgr2  28114  nbuhgr  28120  iunsnima2  31366  fmlasucdisj  33797  opelco3  34159  funpartfv  34462  tailfb  34781  el3v23  36615  eldm4  36666  eldmcnv  36738  ecin0  36745  brcoss3  36827  refressn  36837  disjlem19  37195  pwslnmlem1  41322  rlimdmafv  45304  dfatsnafv2  45379  dfafv23  45380  dfatdmfcoafv2  45381  rlimdmafv2  45385  uspgrsprfo  45945
  Copyright terms: Public domain W3C validator