Theorem elvd 3435

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431

This theorem is referenced by:  inimasn  6120  predep  6294  dffv3  6836  dmfco  6936  fsnex  7238  2ndconst  8051  curry1  8054  qsel  8743  ralxpmap  8844  domunsn  9065  dif1ennnALT  9187  eqinf  9398  dfacacn  10064  dfac13  10065  intgru  10737  shftfib  15034  rlimdm  15513  mat1scmat  22504  imasnopn  23655  imasncld  23656  imasncls  23657  ustuqtop1  24206  ustuqtop2  24207  ustuqtop3  24208  blval2  24527  mulsval  28101  dfnbgr2  29406  nbuhgr  29412  iunsnima2  32692  gblacfnacd  35284  vonf1owev  35290  fmlasucdisj  35581  opelco3  35957  funpartfv  36127  tailfb  36559  el3v23  38555  eldm4  38602  eldmcnv  38666  ecin0  38673  ecun  38714  ecxrn2  38729  ecqmap  38770  dfpre2  38798  brcoss3  38844  refressn  38854  disjlem19  39225  petseq  39297  pwslnmlem1  43520  rlimdmafv  47625  dfatsnafv2  47700  dfafv23  47701  dfatdmfcoafv2  47702  rlimdmafv2  47706  dfclnbgr2  48299  uspgrsprfo  48624