Theorem elvd 3429

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  Vcvv 3422

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424

This theorem is referenced by:  inimasn  6048  predep  6222  dffv3  6752  dmfco  6846  fsnex  7135  2ndconst  7912  curry1  7915  qsel  8543  ralxpmap  8642  domunsn  8863  dif1enALT  8980  eqinf  9173  dfacacn  9828  dfac13  9829  intgru  10501  shftfib  14711  rlimdm  15188  mat1scmat  21596  imasnopn  22749  imasncld  22750  imasncls  22751  ustuqtop1  23301  ustuqtop2  23302  ustuqtop3  23303  blval2  23624  dfnbgr2  27607  nbuhgr  27613  iunsnima2  30860  fmlasucdisj  33261  opelco3  33655  funpartfv  34174  tailfb  34493  el3v23  36304  eldm4  36336  eldmcnv  36407  ecin0  36411  brcoss3  36483  pwslnmlem1  40833  rlimdmafv  44556  dfatsnafv2  44631  dfafv23  44632  dfatdmfcoafv2  44633  rlimdmafv2  44637  uspgrsprfo  45198