Theorem elvd 3446

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2083  Vcvv 3440

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1766  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-v 3442

This theorem is referenced by:  inimasn  5896  predep  6056  dffv3  6541  dmfco  6631  fsnex  6911  2ndconst  7659  curry1  7662  qsel  8233  ralxpmap  8316  domunsn  8521  dif1en  8604  eqinf  8801  dfacacn  9420  dfac13  9421  intgru  10089  shftfib  14269  rlimdm  14746  mat1scmat  20836  imasnopn  21986  imasncld  21987  imasncls  21988  ustuqtop1  22537  ustuqtop2  22538  ustuqtop3  22539  blval2  22859  dfnbgr2  26806  nbuhgr  26812  fmlasucdisj  32256  opelco3  32628  funpartfv  33017  tailfb  33336  el3v23  35050  eldm4  35084  eldmcnv  35155  ecin0  35159  brcoss3  35230  pwslnmlem1  39198  rlimdmafv  42914  dfatsnafv2  42989  dfafv23  42990  dfatdmfcoafv2  42991  rlimdmafv2  42995  uspgrsprfo  43527