Theorem elvd 3460

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2147  Vcvv 3454

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456

This theorem is used by:  inimasn  6159  predep  6354  dffv3  6907  dmfco  7007  fsnex  7317  2ndconst  8142  curry1  8145  qsel  8848  ralxpmap  8955  domunsn  9177  dif1ennnALT  9299  eqinf  9507  dfacacn  10250  dfac13  10251  intgru  10929  shftfib  15257  rlimdm  15750  mat1scmat  22887  imasnopn  24042  imasncld  24043  imasncls  24044  ustuqtop1  24593  ustuqtop2  24594  ustuqtop3  24595  blval2  24914  mulsval  28528  dfnbgr2  29951  nbuhgr  29957  iunsnima2  33288  gblacfnacd  36042  vonf1wev  36049  vonf1owevOLD  36051  vonf1oonfo  36062  onf1oracwevd  36065  onprcf1of1orbd  36067  srepdflem2  36099  fmlasucdisj  36344  opelco3  36730  funpartfv  36900  tailfb  37356  el3v23  39369  eldm4  39416  eldmcnv  39480  ecin0  39487  ecun  39528  ecxrn2  39543  ecqmap  39584  dfpre2  39612  brcoss3  39658  refressn  39668  disjlem19  40039  petseq  40111  pwslnmlem1  44298  rlimdmafv  48462  dfatsnafv2  48537  dfafv23  48538  dfatdmfcoafv2  48539  rlimdmafv2  48543  dfclnbgr2  49136  uspgrsprfo  49461