Theorem elvd 3484

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2106  Vcvv 3478

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480

This theorem is referenced by:  inimasn  6178  predep  6353  dffv3  6903  dmfco  7005  fsnex  7303  2ndconst  8125  curry1  8128  qsel  8835  ralxpmap  8935  domunsn  9166  dif1ennnALT  9309  eqinf  9522  dfacacn  10180  dfac13  10181  intgru  10852  shftfib  15108  rlimdm  15584  mat1scmat  22561  imasnopn  23714  imasncld  23715  imasncls  23716  ustuqtop1  24266  ustuqtop2  24267  ustuqtop3  24268  blval2  24591  mulsval  28150  dfnbgr2  29369  nbuhgr  29375  iunsnima2  32639  gblacfnacd  35092  fmlasucdisj  35384  opelco3  35756  funpartfv  35927  tailfb  36360  el3v23  38209  eldm4  38256  eldmcnv  38327  ecin0  38334  brcoss3  38415  refressn  38425  disjlem19  38783  pwslnmlem1  43081  rlimdmafv  47127  dfatsnafv2  47202  dfafv23  47203  dfatdmfcoafv2  47204  rlimdmafv2  47208  dfclnbgr2  47748  uspgrsprfo  47992