Theorem elvd 3456

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452

This theorem is used by:  inimasn  6145  predep  6333  dffv3  6882  dmfco  6982  fsnex  7292  2ndconst  8115  curry1  8118  qsel  8821  ralxpmap  8928  domunsn  9150  dif1ennnALT  9272  eqinf  9481  dfacacn  10224  dfac13  10225  intgru  10903  shftfib  15231  rlimdm  15724  mat1scmat  22860  imasnopn  24015  imasncld  24016  imasncls  24017  ustuqtop1  24566  ustuqtop2  24567  ustuqtop3  24568  blval2  24887  mulsval  28501  dfnbgr2  29924  nbuhgr  29930  iunsnima2  33261  gblacfnacd  35949  vonf1wev  35956  vonf1owevOLD  35958  vonf1oonfo  35969  onf1oracwevd  35972  onprcf1of1orbd  35974  srepdflem2  36006  fmlasucdisj  36251  opelco3  36632  funpartfv  36802  tailfb  37258  el3v23  39260  eldm4  39307  eldmcnv  39371  ecin0  39378  ecun  39419  ecxrn2  39434  ecqmap  39475  dfpre2  39503  brcoss3  39549  refressn  39559  disjlem19  39930  petseq  40002  pwslnmlem1  44188  rlimdmafv  48341  dfatsnafv2  48416  dfafv23  48417  dfatdmfcoafv2  48418  rlimdmafv2  48422  dfclnbgr2  49015  uspgrsprfo  49340