Theorem elvd 3468

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

Syntax hints:   → wi 4   ∧ wa 394   ∈ wcel 2098  Vcvv 3461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-v 3463

This theorem is referenced by:  inimasn  6162  predep  6338  dffv3  6892  dmfco  6993  fsnex  7292  2ndconst  8106  curry1  8109  qsel  8815  ralxpmap  8915  domunsn  9152  dif1ennnALT  9302  eqinf  9509  dfacacn  10166  dfac13  10167  intgru  10839  shftfib  15055  rlimdm  15531  mat1scmat  22485  imasnopn  23638  imasncld  23639  imasncls  23640  ustuqtop1  24190  ustuqtop2  24191  ustuqtop3  24192  blval2  24515  mulsval  28059  dfnbgr2  29222  nbuhgr  29228  iunsnima2  32488  fmlasucdisj  35140  opelco3  35501  funpartfv  35672  tailfb  35992  el3v23  37828  eldm4  37876  eldmcnv  37947  ecin0  37954  brcoss3  38035  refressn  38045  disjlem19  38403  pwslnmlem1  42658  rlimdmafv  46695  dfatsnafv2  46770  dfafv23  46771  dfatdmfcoafv2  46772  rlimdmafv2  46776  dfclnbgr2  47300  uspgrsprfo  47396