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  22733  imasnopn  23884  imasncld  23885  imasncls  23886  ustuqtop1  24435  ustuqtop2  24436  ustuqtop3  24437  blval2  24756  mulsval  28339  dfnbgr2  29724  nbuhgr  29730  iunsnima2  33001  gblacfnacd  35610  vonf1wev  35616  vonf1owevOLD  35618  vonf1oonfo  35623  fmlasucdisj  35912  opelco3  36288  funpartfv  36458  tailfb  36929  el3v23  38924  eldm4  38971  eldmcnv  39035  ecin0  39042  ecun  39083  ecxrn2  39098  ecqmap  39139  dfpre2  39167  brcoss3  39213  refressn  39223  disjlem19  39594  petseq  39666  pwslnmlem1  43860  rlimdmafv  47955  dfatsnafv2  48030  dfafv23  48031  dfatdmfcoafv2  48032  rlimdmafv2  48036  dfclnbgr2  48629  uspgrsprfo  48954