Theorem elvd 3463

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2145  Vcvv 3457

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459

This theorem is referenced by:  inimasn  6144  predep  6320  dffv3  6867  dmfco  6967  fsnex  7271  2ndconst  8084  curry1  8087  qsel  8782  ralxpmap  8882  domunsn  9103  dif1ennnALT  9225  eqinf  9433  dfacacn  10113  dfac13  10114  intgru  10787  shftfib  15097  rlimdm  15590  mat1scmat  22653  imasnopn  23804  imasncld  23805  imasncls  23806  ustuqtop1  24355  ustuqtop2  24356  ustuqtop3  24357  blval2  24676  mulsval  28256  dfnbgr2  29592  nbuhgr  29598  iunsnima2  32872  gblacfnacd  35452  vonf1wev  35458  vonf1owevOLD  35460  vonf1oonfo  35465  fmlasucdisj  35757  opelco3  36133  funpartfv  36303  tailfb  36745  el3v23  38740  eldm4  38787  eldmcnv  38851  ecin0  38858  ecun  38899  ecxrn2  38914  ecqmap  38955  dfpre2  38983  brcoss3  39029  refressn  39039  disjlem19  39410  petseq  39482  pwslnmlem1  43676  rlimdmafv  47770  dfatsnafv2  47845  dfafv23  47846  dfatdmfcoafv2  47847  rlimdmafv2  47851  dfclnbgr2  48444  uspgrsprfo  48769