Theorem elvd 3481

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  Vcvv 3474

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476

This theorem is referenced by:  inimasn  6155  predep  6331  dffv3  6887  dmfco  6987  fsnex  7283  2ndconst  8089  curry1  8092  qsel  8792  ralxpmap  8892  domunsn  9129  dif1ennnALT  9279  eqinf  9481  dfacacn  10138  dfac13  10139  intgru  10811  shftfib  15021  rlimdm  15497  mat1scmat  22048  imasnopn  23201  imasncld  23202  imasncls  23203  ustuqtop1  23753  ustuqtop2  23754  ustuqtop3  23755  blval2  24078  mulsval  27575  dfnbgr2  28632  nbuhgr  28638  iunsnima2  31886  fmlasucdisj  34459  opelco3  34821  funpartfv  34992  tailfb  35354  el3v23  37184  eldm4  37234  eldmcnv  37306  ecin0  37313  brcoss3  37395  refressn  37405  disjlem19  37763  pwslnmlem1  41922  rlimdmafv  45970  dfatsnafv2  46045  dfafv23  46046  dfatdmfcoafv2  46047  rlimdmafv2  46051  uspgrsprfo  46611