Theorem elvd 3482

Description: If a proposition is implied by 𝑥 ∈ V (which is true, see vex 3479) and another antecedent, then it is implied by that other antecedent. Deduction associated with elv 3481. (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 3479	. 2 ⊢ 𝑥 ∈ V
2		elvd.1	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ V) → 𝜓)
3	1, 2	mpan2 690	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107  Vcvv 3475

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 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477

This theorem is referenced by:  inimasn  6156  predep  6332  dffv3  6888  dmfco  6988  fsnex  7281  2ndconst  8087  curry1  8090  qsel  8790  ralxpmap  8890  domunsn  9127  dif1ennnALT  9277  eqinf  9479  dfacacn  10136  dfac13  10137  intgru  10809  shftfib  15019  rlimdm  15495  mat1scmat  22041  imasnopn  23194  imasncld  23195  imasncls  23196  ustuqtop1  23746  ustuqtop2  23747  ustuqtop3  23748  blval2  24071  mulsval  27565  dfnbgr2  28594  nbuhgr  28600  iunsnima2  31848  fmlasucdisj  34390  opelco3  34746  funpartfv  34917  tailfb  35262  el3v23  37092  eldm4  37142  eldmcnv  37214  ecin0  37221  brcoss3  37303  refressn  37313  disjlem19  37671  pwslnmlem1  41834  rlimdmafv  45885  dfatsnafv2  45960  dfafv23  45961  dfatdmfcoafv2  45962  rlimdmafv2  45966  uspgrsprfo  46526