Theorem elvd 3444

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  Vcvv 3438

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 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440

This theorem is referenced by:  inimasn  6109  predep  6282  dffv3  6822  dmfco  6923  fsnex  7224  2ndconst  8041  curry1  8044  qsel  8730  ralxpmap  8830  domunsn  9051  dif1ennnALT  9180  eqinf  9394  dfacacn  10055  dfac13  10056  intgru  10727  shftfib  14997  rlimdm  15476  mat1scmat  22442  imasnopn  23593  imasncld  23594  imasncls  23595  ustuqtop1  24145  ustuqtop2  24146  ustuqtop3  24147  blval2  24466  mulsval  28035  dfnbgr2  29300  nbuhgr  29306  iunsnima2  32580  gblacfnacd  35074  vonf1owev  35080  fmlasucdisj  35371  opelco3  35747  funpartfv  35918  tailfb  36350  el3v23  38201  eldm4  38248  eldmcnv  38312  ecin0  38319  brcoss3  38409  refressn  38419  disjlem19  38778  pwslnmlem1  43065  rlimdmafv  47162  dfatsnafv2  47237  dfafv23  47238  dfatdmfcoafv2  47239  rlimdmafv2  47243  dfclnbgr2  47808  uspgrsprfo  48133