Theorem elvd 3453

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  Vcvv 3446

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448

This theorem is referenced by:  inimasn  6113  predep  6289  dffv3  6843  dmfco  6942  fsnex  7234  2ndconst  8038  curry1  8041  qsel  8742  ralxpmap  8841  domunsn  9078  dif1ennnALT  9228  eqinf  9429  dfacacn  10086  dfac13  10087  intgru  10759  shftfib  14969  rlimdm  15445  mat1scmat  21925  imasnopn  23078  imasncld  23079  imasncls  23080  ustuqtop1  23630  ustuqtop2  23631  ustuqtop3  23632  blval2  23955  mulsval  27417  dfnbgr2  28348  nbuhgr  28354  iunsnima2  31605  fmlasucdisj  34080  opelco3  34435  funpartfv  34606  tailfb  34925  el3v23  36756  eldm4  36807  eldmcnv  36879  ecin0  36886  brcoss3  36968  refressn  36978  disjlem19  37336  pwslnmlem1  41477  rlimdmafv  45529  dfatsnafv2  45604  dfafv23  45605  dfatdmfcoafv2  45606  rlimdmafv2  45610  uspgrsprfo  46170