Theorem elvd 3461

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143  Vcvv 3455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457

This theorem is referenced by:  inimasn  6155  predep  6333  dffv3  6879  dmfco  6979  fsnex  7283  2ndconst  8097  curry1  8100  qsel  8795  ralxpmap  8895  domunsn  9116  dif1ennnALT  9238  eqinf  9446  dfacacn  10126  dfac13  10127  intgru  10800  shftfib  15111  rlimdm  15604  mat1scmat  22677  imasnopn  23828  imasncld  23829  imasncls  23830  ustuqtop1  24379  ustuqtop2  24380  ustuqtop3  24381  blval2  24700  mulsval  28283  dfnbgr2  29668  nbuhgr  29674  iunsnima2  32945  gblacfnacd  35567  vonf1wev  35573  vonf1owevOLD  35575  vonf1oonfo  35580  fmlasucdisj  35872  opelco3  36248  funpartfv  36418  tailfb  36869  el3v23  38864  eldm4  38911  eldmcnv  38975  ecin0  38982  ecun  39023  ecxrn2  39038  ecqmap  39079  dfpre2  39107  brcoss3  39153  refressn  39163  disjlem19  39534  petseq  39606  pwslnmlem1  43802  rlimdmafv  47897  dfatsnafv2  47972  dfafv23  47973  dfatdmfcoafv2  47974  rlimdmafv2  47978  dfclnbgr2  48571  uspgrsprfo  48896