Theorem elvd 3503

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2113  Vcvv 3497

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1780  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3499

This theorem is referenced by:  inimasn  6016  predep  6177  dffv3  6669  dmfco  6760  fsnex  7042  2ndconst  7799  curry1  7802  qsel  8379  ralxpmap  8463  domunsn  8670  dif1en  8754  eqinf  8951  dfacacn  9570  dfac13  9571  intgru  10239  shftfib  14434  rlimdm  14911  mat1scmat  21151  imasnopn  22301  imasncld  22302  imasncls  22303  ustuqtop1  22853  ustuqtop2  22854  ustuqtop3  22855  blval2  23175  dfnbgr2  27122  nbuhgr  27128  fmlasucdisj  32650  opelco3  33022  funpartfv  33410  tailfb  33729  el3v23  35501  eldm4  35535  eldmcnv  35606  ecin0  35610  brcoss3  35682  pwslnmlem1  39698  rlimdmafv  43383  dfatsnafv2  43458  dfafv23  43459  dfatdmfcoafv2  43460  rlimdmafv2  43464  uspgrsprfo  44030