Theorem elvd 3391

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

Syntax hints:   → wi 4   ∧ wa 385   ∈ wcel 2157  Vcvv 3386

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-12 2213  ax-ext 2778

This theorem depends on definitions:  df-bi 199  df-an 386  df-tru 1657  df-ex 1876  df-sb 2065  df-clab 2787  df-cleq 2793  df-clel 2796  df-v 3388

This theorem is referenced by:  inimasn  5768  predep  5925  dffv3  6408  dmfco  6498  fsnex  6767  2ndconst  7504  curry1  7507  qsel  8065  ralxpmap  8148  domunsn  8353  dif1en  8436  eqinf  8633  dfacacn  9252  dfac13  9253  intgru  9925  shftfib  14152  rlimdm  14622  mat1scmat  20670  imasnopn  21821  imasncld  21822  imasncls  21823  ustuqtop1  22372  ustuqtop2  22373  ustuqtop3  22374  blval2  22694  dfnbgr2  26571  nbuhgr  26580  opelco3  32189  funpartfv  32564  tailfb  32883  el3v23  34498  eldm4  34533  eldmcnv  34606  ecin0  34610  brcoss3  34681  pwslnmlem1  38442  rlimdmafv  42026  dfatsnafv2  42101  dfafv23  42102  dfatdmfcoafv2  42103  rlimdmafv2  42107  uspgrsprfo  42550