Theorem elvd 3442

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2102  Vcvv 3435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2104  ax-9 2112  ax-ext 2705

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1540  df-ex 1778  df-sb 2064  df-clab 2712  df-cleq 2726  df-clel 2812  df-v 3437

This theorem is referenced by:  inimasn  6069  predep  6243  dffv3  6795  dmfco  6891  fsnex  7182  2ndconst  7968  curry1  7971  qsel  8612  ralxpmap  8711  domunsn  8946  dif1enALT  9085  eqinf  9278  dfacacn  9932  dfac13  9933  intgru  10605  shftfib  14818  rlimdm  15295  mat1scmat  21723  imasnopn  22876  imasncld  22877  imasncls  22878  ustuqtop1  23428  ustuqtop2  23429  ustuqtop3  23430  blval2  23753  dfnbgr2  27739  nbuhgr  27745  iunsnima2  30994  fmlasucdisj  33396  opelco3  33784  funpartfv  34282  tailfb  34601  el3v23  36412  eldm4  36443  eldmcnv  36513  ecin0  36517  brcoss3  36589  pwslnmlem1  40948  rlimdmafv  44716  dfatsnafv2  44791  dfafv23  44792  dfatdmfcoafv2  44793  rlimdmafv2  44797  uspgrsprfo  45357