Theorem elvd 3500

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2114  Vcvv 3494

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-v 3496

This theorem is referenced by:  inimasn  6013  predep  6174  dffv3  6666  dmfco  6757  fsnex  7039  2ndconst  7796  curry1  7799  qsel  8376  ralxpmap  8460  domunsn  8667  dif1en  8751  eqinf  8948  dfacacn  9567  dfac13  9568  intgru  10236  shftfib  14431  rlimdm  14908  mat1scmat  21148  imasnopn  22298  imasncld  22299  imasncls  22300  ustuqtop1  22850  ustuqtop2  22851  ustuqtop3  22852  blval2  23172  dfnbgr2  27119  nbuhgr  27125  fmlasucdisj  32646  opelco3  33018  funpartfv  33406  tailfb  33725  el3v23  35512  eldm4  35546  eldmcnv  35617  ecin0  35621  brcoss3  35693  pwslnmlem1  39741  rlimdmafv  43425  dfatsnafv2  43500  dfafv23  43501  dfatdmfcoafv2  43502  rlimdmafv2  43506  uspgrsprfo  44072