Theorem elvd 3438

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119  Vcvv 3432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434

This theorem is referenced by:  inimasn  6114  predep  6288  dffv3  6830  dmfco  6930  fsnex  7234  2ndconst  8047  curry1  8050  qsel  8740  ralxpmap  8841  domunsn  9062  dif1ennnALT  9184  eqinf  9395  dfacacn  10062  dfac13  10063  intgru  10735  shftfib  15032  rlimdm  15511  mat1scmat  22529  imasnopn  23680  imasncld  23681  imasncls  23682  ustuqtop1  24231  ustuqtop2  24232  ustuqtop3  24233  blval2  24552  mulsval  28126  dfnbgr2  29431  nbuhgr  29437  iunsnima2  32718  gblacfnacd  35337  vonf1owev  35343  fmlasucdisj  35634  opelco3  36010  funpartfv  36180  tailfb  36612  el3v23  38608  eldm4  38655  eldmcnv  38719  ecin0  38726  ecun  38767  ecxrn2  38782  ecqmap  38823  dfpre2  38851  brcoss3  38897  refressn  38907  disjlem19  39278  petseq  39350  pwslnmlem1  43544  rlimdmafv  47647  dfatsnafv2  47722  dfafv23  47723  dfatdmfcoafv2  47724  rlimdmafv2  47728  dfclnbgr2  48321  uspgrsprfo  48646