Theorem elvd 3405

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2112  Vcvv 3398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400

This theorem is referenced by:  inimasn  5999  predep  6166  dffv3  6691  dmfco  6785  fsnex  7071  2ndconst  7847  curry1  7850  qsel  8456  ralxpmap  8555  domunsn  8774  dif1enOLD  8885  eqinf  9078  dfacacn  9720  dfac13  9721  intgru  10393  shftfib  14600  rlimdm  15077  mat1scmat  21390  imasnopn  22541  imasncld  22542  imasncls  22543  ustuqtop1  23093  ustuqtop2  23094  ustuqtop3  23095  blval2  23414  dfnbgr2  27379  nbuhgr  27385  iunsnima2  30632  fmlasucdisj  33028  opelco3  33419  funpartfv  33933  tailfb  34252  el3v23  36063  eldm4  36095  eldmcnv  36166  ecin0  36170  brcoss3  36242  pwslnmlem1  40561  rlimdmafv  44284  dfatsnafv2  44359  dfafv23  44360  dfatdmfcoafv2  44361  rlimdmafv2  44365  uspgrsprfo  44926