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

Theorem elvd 3450
Description: If a proposition is implied by 𝑥 ∈ V (which is true, see vex 3447) and another antecedent, then it is implied by that other antecedent. Deduction associated with elv 3449. (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 3447 . 2 𝑥 ∈ V
2 elvd.1 . 2 ((𝜑𝑥 ∈ V) → 𝜓)
31, 2mpan2 690 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wcel 2112  Vcvv 3444
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-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446
This theorem is referenced by:  inimasn  5984  predep  6146  dffv3  6645  dmfco  6738  fsnex  7021  2ndconst  7783  curry1  7786  qsel  8363  ralxpmap  8447  domunsn  8655  dif1en  8739  eqinf  8936  dfacacn  9556  dfac13  9557  intgru  10229  shftfib  14426  rlimdm  14903  mat1scmat  21147  imasnopn  22298  imasncld  22299  imasncls  22300  ustuqtop1  22850  ustuqtop2  22851  ustuqtop3  22852  blval2  23172  dfnbgr2  27130  nbuhgr  27136  iunsnima2  30386  fmlasucdisj  32754  opelco3  33126  funpartfv  33514  tailfb  33833  el3v23  35650  eldm4  35684  eldmcnv  35755  ecin0  35759  brcoss3  35831  pwslnmlem1  40023  rlimdmafv  43720  dfatsnafv2  43795  dfafv23  43796  dfatdmfcoafv2  43797  rlimdmafv2  43801  uspgrsprfo  44363
  Copyright terms: Public domain W3C validator