Theorem elvd 3453

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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449

This theorem is referenced by:  inimasn  6129  predep  6303  dffv3  6854  dmfco  6957  fsnex  7258  2ndconst  8080  curry1  8083  qsel  8769  ralxpmap  8869  domunsn  9091  dif1ennnALT  9222  eqinf  9436  dfacacn  10095  dfac13  10096  intgru  10767  shftfib  15038  rlimdm  15517  mat1scmat  22426  imasnopn  23577  imasncld  23578  imasncls  23579  ustuqtop1  24129  ustuqtop2  24130  ustuqtop3  24131  blval2  24450  mulsval  28012  dfnbgr2  29264  nbuhgr  29270  iunsnima2  32547  gblacfnacd  35089  vonf1owev  35095  fmlasucdisj  35386  opelco3  35762  funpartfv  35933  tailfb  36365  el3v23  38216  eldm4  38263  eldmcnv  38327  ecin0  38334  brcoss3  38424  refressn  38434  disjlem19  38793  pwslnmlem1  43081  rlimdmafv  47178  dfatsnafv2  47253  dfafv23  47254  dfatdmfcoafv2  47255  rlimdmafv2  47259  dfclnbgr2  47824  uspgrsprfo  48136