Theorem elvd 3470

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466

This theorem is referenced by:  inimasn  6150  predep  6324  dffv3  6877  dmfco  6980  fsnex  7281  2ndconst  8105  curry1  8108  qsel  8815  ralxpmap  8915  domunsn  9146  dif1ennnALT  9288  eqinf  9502  dfacacn  10161  dfac13  10162  intgru  10833  shftfib  15096  rlimdm  15572  mat1scmat  22482  imasnopn  23633  imasncld  23634  imasncls  23635  ustuqtop1  24185  ustuqtop2  24186  ustuqtop3  24187  blval2  24506  mulsval  28069  dfnbgr2  29321  nbuhgr  29327  iunsnima2  32604  gblacfnacd  35135  fmlasucdisj  35426  opelco3  35797  funpartfv  35968  tailfb  36400  el3v23  38251  eldm4  38297  eldmcnv  38368  ecin0  38375  brcoss3  38456  refressn  38466  disjlem19  38824  pwslnmlem1  43083  rlimdmafv  47173  dfatsnafv2  47248  dfafv23  47249  dfatdmfcoafv2  47250  rlimdmafv2  47254  dfclnbgr2  47804  uspgrsprfo  48090