Theorem elvd 3485

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2107  Vcvv 3479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481

This theorem is referenced by:  inimasn  6175  predep  6350  dffv3  6901  dmfco  7004  fsnex  7304  2ndconst  8127  curry1  8130  qsel  8837  ralxpmap  8937  domunsn  9168  dif1ennnALT  9312  eqinf  9525  dfacacn  10183  dfac13  10184  intgru  10855  shftfib  15112  rlimdm  15588  mat1scmat  22546  imasnopn  23699  imasncld  23700  imasncls  23701  ustuqtop1  24251  ustuqtop2  24252  ustuqtop3  24253  blval2  24576  mulsval  28136  dfnbgr2  29355  nbuhgr  29361  iunsnima2  32632  gblacfnacd  35114  fmlasucdisj  35405  opelco3  35776  funpartfv  35947  tailfb  36379  el3v23  38230  eldm4  38276  eldmcnv  38347  ecin0  38354  brcoss3  38435  refressn  38445  disjlem19  38803  pwslnmlem1  43109  rlimdmafv  47194  dfatsnafv2  47269  dfafv23  47270  dfatdmfcoafv2  47271  rlimdmafv2  47275  dfclnbgr2  47815  uspgrsprfo  48069