Theorem elvd 3459

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  Vcvv 3453

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455

This theorem is used by:  inimasn  6151  predep  6332  dffv3  6878  dmfco  6978  fsnex  7288  2ndconst  8102  curry1  8105  qsel  8800  ralxpmap  8907  domunsn  9129  dif1ennnALT  9251  eqinf  9459  dfacacn  10148  dfac13  10149  intgru  10827  shftfib  15149  rlimdm  15642  mat1scmat  22767  imasnopn  23922  imasncld  23923  imasncls  23924  ustuqtop1  24473  ustuqtop2  24474  ustuqtop3  24475  blval2  24794  mulsval  28382  dfnbgr2  29805  nbuhgr  29811  iunsnima2  33100  gblacfnacd  35707  vonf1wev  35713  vonf1owevOLD  35715  vonf1oonfo  35720  fmlasucdisj  35986  opelco3  36362  funpartfv  36532  tailfb  37004  el3v23  38990  eldm4  39037  eldmcnv  39101  ecin0  39108  ecun  39149  ecxrn2  39164  ecqmap  39205  dfpre2  39233  brcoss3  39279  refressn  39289  disjlem19  39660  petseq  39732  pwslnmlem1  43941  rlimdmafv  48073  dfatsnafv2  48148  dfafv23  48149  dfatdmfcoafv2  48150  rlimdmafv2  48154  dfclnbgr2  48747  uspgrsprfo  49072