Theorem elvd 3446

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  Vcvv 3440

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 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442

This theorem is referenced by:  inimasn  6114  predep  6288  dffv3  6830  dmfco  6930  fsnex  7229  2ndconst  8043  curry1  8046  qsel  8733  ralxpmap  8834  domunsn  9055  dif1ennnALT  9177  eqinf  9388  dfacacn  10052  dfac13  10053  intgru  10725  shftfib  14995  rlimdm  15474  mat1scmat  22483  imasnopn  23634  imasncld  23635  imasncls  23636  ustuqtop1  24185  ustuqtop2  24186  ustuqtop3  24187  blval2  24506  mulsval  28105  dfnbgr2  29410  nbuhgr  29416  iunsnima2  32697  gblacfnacd  35296  vonf1owev  35302  fmlasucdisj  35593  opelco3  35969  funpartfv  36139  tailfb  36571  el3v23  38426  eldm4  38470  eldmcnv  38534  ecin0  38541  ecun  38574  ecxrn2  38589  dfpre2  38647  brcoss3  38692  refressn  38702  disjlem19  39056  pwslnmlem1  43330  rlimdmafv  47419  dfatsnafv2  47494  dfafv23  47495  dfatdmfcoafv2  47496  rlimdmafv2  47500  dfclnbgr2  48065  uspgrsprfo  48390