Theorem elvd 3494

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  Vcvv 3488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490

This theorem is referenced by:  inimasn  6187  predep  6362  dffv3  6916  dmfco  7018  fsnex  7319  2ndconst  8142  curry1  8145  qsel  8854  ralxpmap  8954  domunsn  9193  dif1ennnALT  9339  eqinf  9553  dfacacn  10211  dfac13  10212  intgru  10883  shftfib  15121  rlimdm  15597  mat1scmat  22566  imasnopn  23719  imasncld  23720  imasncls  23721  ustuqtop1  24271  ustuqtop2  24272  ustuqtop3  24273  blval2  24596  mulsval  28153  dfnbgr2  29372  nbuhgr  29378  iunsnima2  32641  gblacfnacd  35075  fmlasucdisj  35367  opelco3  35738  funpartfv  35909  tailfb  36343  el3v23  38182  eldm4  38230  eldmcnv  38301  ecin0  38308  brcoss3  38389  refressn  38399  disjlem19  38757  pwslnmlem1  43049  rlimdmafv  47092  dfatsnafv2  47167  dfafv23  47168  dfatdmfcoafv2  47169  rlimdmafv2  47173  dfclnbgr2  47697  uspgrsprfo  47871