Theorem elvd 3457

Description: If a proposition is implied by 𝑥 ∈ V (which is true, see vex 3455) and another antecedent, then it is implied by that other antecedent. Deduction associated with elv 3456. (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 3455	. 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 3451

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453

This theorem is used by:  inimasn  6145  predep  6326  dffv3  6873  dmfco  6973  fsnex  7283  2ndconst  8101  curry1  8104  qsel  8801  ralxpmap  8908  domunsn  9130  dif1ennnALT  9252  eqinf  9461  dfacacn  10201  dfac13  10202  intgru  10880  shftfib  15205  rlimdm  15698  mat1scmat  22834  imasnopn  23989  imasncld  23990  imasncls  23991  ustuqtop1  24540  ustuqtop2  24541  ustuqtop3  24542  blval2  24861  mulsval  28477  dfnbgr2  29900  nbuhgr  29906  iunsnima2  33195  gblacfnacd  35854  vonf1wev  35860  vonf1owevOLD  35862  vonf1oonfo  35867  fmlasucdisj  36133  opelco3  36509  funpartfv  36679  tailfb  37135  el3v23  39134  eldm4  39181  eldmcnv  39245  ecin0  39252  ecun  39293  ecxrn2  39308  ecqmap  39349  dfpre2  39377  brcoss3  39423  refressn  39433  disjlem19  39804  petseq  39876  pwslnmlem1  44052  rlimdmafv  48191  dfatsnafv2  48266  dfafv23  48267  dfatdmfcoafv2  48268  rlimdmafv2  48272  dfclnbgr2  48865  uspgrsprfo  49190