Theorem elvd 3448

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

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

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 3444

This theorem is referenced by:  inimasn  6122  predep  6296  dffv3  6838  dmfco  6938  fsnex  7239  2ndconst  8053  curry1  8056  qsel  8745  ralxpmap  8846  domunsn  9067  dif1ennnALT  9189  eqinf  9400  dfacacn  10064  dfac13  10065  intgru  10737  shftfib  15007  rlimdm  15486  mat1scmat  22495  imasnopn  23646  imasncld  23647  imasncls  23648  ustuqtop1  24197  ustuqtop2  24198  ustuqtop3  24199  blval2  24518  mulsval  28117  dfnbgr2  29422  nbuhgr  29428  iunsnima2  32708  gblacfnacd  35315  vonf1owev  35321  fmlasucdisj  35612  opelco3  35988  funpartfv  36158  tailfb  36590  el3v23  38479  eldm4  38526  eldmcnv  38590  ecin0  38597  ecun  38638  ecxrn2  38653  ecqmap  38694  dfpre2  38722  brcoss3  38768  refressn  38778  disjlem19  39149  petseq  39221  pwslnmlem1  43443  rlimdmafv  47531  dfatsnafv2  47606  dfafv23  47607  dfatdmfcoafv2  47608  rlimdmafv2  47612  dfclnbgr2  48177  uspgrsprfo  48502