Theorem elvd 3436

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  Vcvv 3430

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432

This theorem is referenced by:  inimasn  6114  predep  6288  dffv3  6830  dmfco  6930  fsnex  7231  2ndconst  8044  curry1  8047  qsel  8736  ralxpmap  8837  domunsn  9058  dif1ennnALT  9180  eqinf  9391  dfacacn  10055  dfac13  10056  intgru  10728  shftfib  15025  rlimdm  15504  mat1scmat  22514  imasnopn  23665  imasncld  23666  imasncls  23667  ustuqtop1  24216  ustuqtop2  24217  ustuqtop3  24218  blval2  24537  mulsval  28115  dfnbgr2  29420  nbuhgr  29426  iunsnima2  32707  gblacfnacd  35300  vonf1owev  35306  fmlasucdisj  35597  opelco3  35973  funpartfv  36143  tailfb  36575  el3v23  38569  eldm4  38616  eldmcnv  38680  ecin0  38687  ecun  38728  ecxrn2  38743  ecqmap  38784  dfpre2  38812  brcoss3  38858  refressn  38868  disjlem19  39239  petseq  39311  pwslnmlem1  43538  rlimdmafv  47637  dfatsnafv2  47712  dfafv23  47713  dfatdmfcoafv2  47714  rlimdmafv2  47718  dfclnbgr2  48311  uspgrsprfo  48636