Theorem elvd 3464

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

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

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 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460

This theorem is used by:  inimasn  6158  predep  6338  dffv3  6884  dmfco  6984  fsnex  7292  2ndconst  8105  curry1  8108  qsel  8803  ralxpmap  8903  domunsn  9125  dif1ennnALT  9247  eqinf  9455  dfacacn  10144  dfac13  10145  intgru  10817  shftfib  15135  rlimdm  15628  mat1scmat  22726  imasnopn  23877  imasncld  23878  imasncls  23879  ustuqtop1  24428  ustuqtop2  24429  ustuqtop3  24430  blval2  24749  mulsval  28332  dfnbgr2  29717  nbuhgr  29723  iunsnima2  32994  gblacfnacd  35602  vonf1wev  35608  vonf1owevOLD  35610  vonf1oonfo  35615  fmlasucdisj  35904  opelco3  36280  funpartfv  36450  tailfb  36921  el3v23  38916  eldm4  38963  eldmcnv  39027  ecin0  39034  ecun  39075  ecxrn2  39090  ecqmap  39131  dfpre2  39159  brcoss3  39205  refressn  39215  disjlem19  39586  petseq  39658  pwslnmlem1  43852  rlimdmafv  47947  dfatsnafv2  48022  dfafv23  48023  dfatdmfcoafv2  48024  rlimdmafv2  48028  dfclnbgr2  48621  uspgrsprfo  48946