Theorem elvd 3443

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  Vcvv 3437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439

This theorem is referenced by:  inimasn  6108  predep  6282  dffv3  6824  dmfco  6924  fsnex  7223  2ndconst  8037  curry1  8040  qsel  8726  ralxpmap  8826  domunsn  9047  dif1ennnALT  9168  eqinf  9376  dfacacn  10040  dfac13  10041  intgru  10712  shftfib  14981  rlimdm  15460  mat1scmat  22455  imasnopn  23606  imasncld  23607  imasncls  23608  ustuqtop1  24157  ustuqtop2  24158  ustuqtop3  24159  blval2  24478  mulsval  28049  dfnbgr2  29317  nbuhgr  29323  iunsnima2  32604  gblacfnacd  35167  vonf1owev  35173  fmlasucdisj  35464  opelco3  35840  funpartfv  36010  tailfb  36442  el3v23  38289  eldm4  38333  eldmcnv  38397  ecin0  38404  ecun  38437  ecxrn2  38452  dfpre2  38510  brcoss3  38555  refressn  38565  disjlem19  38919  pwslnmlem1  43209  rlimdmafv  47301  dfatsnafv2  47376  dfafv23  47377  dfatdmfcoafv2  47378  rlimdmafv2  47382  dfclnbgr2  47947  uspgrsprfo  48272