Theorem elvd 3442

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111  Vcvv 3436

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438

This theorem is referenced by:  inimasn  6103  predep  6277  dffv3  6818  dmfco  6918  fsnex  7217  2ndconst  8031  curry1  8034  qsel  8720  ralxpmap  8820  domunsn  9040  dif1ennnALT  9161  eqinf  9369  dfacacn  10030  dfac13  10031  intgru  10702  shftfib  14976  rlimdm  15455  mat1scmat  22452  imasnopn  23603  imasncld  23604  imasncls  23605  ustuqtop1  24154  ustuqtop2  24155  ustuqtop3  24156  blval2  24475  mulsval  28046  dfnbgr2  29313  nbuhgr  29319  iunsnima2  32597  gblacfnacd  35134  vonf1owev  35140  fmlasucdisj  35431  opelco3  35807  funpartfv  35978  tailfb  36410  el3v23  38261  eldm4  38308  eldmcnv  38372  ecin0  38379  brcoss3  38469  refressn  38479  disjlem19  38838  pwslnmlem1  43124  rlimdmafv  47207  dfatsnafv2  47282  dfafv23  47283  dfatdmfcoafv2  47284  rlimdmafv2  47288  dfclnbgr2  47853  uspgrsprfo  48178