Theorem elvd 3439

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  Vcvv 3433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3435

This theorem is referenced by:  inimasn  6099  predep  6272  dffv3  6812  dmfco  6912  fsnex  7211  2ndconst  8025  curry1  8028  qsel  8714  ralxpmap  8814  domunsn  9034  dif1ennnALT  9155  eqinf  9363  dfacacn  10024  dfac13  10025  intgru  10696  shftfib  14966  rlimdm  15445  mat1scmat  22408  imasnopn  23559  imasncld  23560  imasncls  23561  ustuqtop1  24110  ustuqtop2  24111  ustuqtop3  24112  blval2  24431  mulsval  28002  dfnbgr2  29269  nbuhgr  29275  iunsnima2  32554  gblacfnacd  35092  vonf1owev  35098  fmlasucdisj  35389  opelco3  35765  funpartfv  35936  tailfb  36368  el3v23  38219  eldm4  38266  eldmcnv  38330  ecin0  38337  brcoss3  38427  refressn  38437  disjlem19  38796  pwslnmlem1  43082  rlimdmafv  47175  dfatsnafv2  47250  dfafv23  47251  dfatdmfcoafv2  47252  rlimdmafv2  47256  dfclnbgr2  47821  uspgrsprfo  48146