Theorem elvd 3456

Description: If a proposition is implied by 𝑥 ∈ V (which is true, see vex 3454) and another antecedent, then it is implied by that other antecedent. Deduction associated with elv 3455. (Contributed by Peter Mazsa, 23-Oct-2018.)

Hypothesis

Ref	Expression
elvd.1	⊢ ((𝜑 ∧ 𝑥 ∈ V) → 𝜓)

Assertion

Ref	Expression
elvd	⊢ (𝜑 → 𝜓)

Proof of Theorem elvd

Step	Hyp	Ref	Expression
1		vex 3454	. 2 ⊢ 𝑥 ∈ V
2		elvd.1	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ V) → 𝜓)
3	1, 2	mpan2 691	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  Vcvv 3450

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452

This theorem is referenced by:  inimasn  6132  predep  6306  dffv3  6857  dmfco  6960  fsnex  7261  2ndconst  8083  curry1  8086  qsel  8772  ralxpmap  8872  domunsn  9097  dif1ennnALT  9229  eqinf  9443  dfacacn  10102  dfac13  10103  intgru  10774  shftfib  15045  rlimdm  15524  mat1scmat  22433  imasnopn  23584  imasncld  23585  imasncls  23586  ustuqtop1  24136  ustuqtop2  24137  ustuqtop3  24138  blval2  24457  mulsval  28019  dfnbgr2  29271  nbuhgr  29277  iunsnima2  32554  gblacfnacd  35096  vonf1owev  35102  fmlasucdisj  35393  opelco3  35769  funpartfv  35940  tailfb  36372  el3v23  38223  eldm4  38270  eldmcnv  38334  ecin0  38341  brcoss3  38431  refressn  38441  disjlem19  38800  pwslnmlem1  43088  rlimdmafv  47182  dfatsnafv2  47257  dfafv23  47258  dfatdmfcoafv2  47259  rlimdmafv2  47263  dfclnbgr2  47828  uspgrsprfo  48140