![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elvd | Structured version Visualization version GIF version |
Description: If a proposition is implied by 𝑥 ∈ V (which is true, see vex 3389) and another antecedent, then it is implied by that other antecedent. Deduction associated with elv 3390. (Contributed by Peter Mazsa, 23-Oct-2018.) |
Ref | Expression |
---|---|
elvd.1 | ⊢ ((𝜑 ∧ 𝑥 ∈ V) → 𝜓) |
Ref | Expression |
---|---|
elvd | ⊢ (𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 3389 | . 2 ⊢ 𝑥 ∈ V | |
2 | elvd.1 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ V) → 𝜓) | |
3 | 1, 2 | mpan2 683 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 385 ∈ wcel 2157 Vcvv 3386 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-12 2213 ax-ext 2778 |
This theorem depends on definitions: df-bi 199 df-an 386 df-tru 1657 df-ex 1876 df-sb 2065 df-clab 2787 df-cleq 2793 df-clel 2796 df-v 3388 |
This theorem is referenced by: inimasn 5768 predep 5925 dffv3 6408 dmfco 6498 fsnex 6767 2ndconst 7504 curry1 7507 qsel 8065 ralxpmap 8148 domunsn 8353 dif1en 8436 eqinf 8633 dfacacn 9252 dfac13 9253 intgru 9925 shftfib 14152 rlimdm 14622 mat1scmat 20670 imasnopn 21821 imasncld 21822 imasncls 21823 ustuqtop1 22372 ustuqtop2 22373 ustuqtop3 22374 blval2 22694 dfnbgr2 26571 nbuhgr 26580 opelco3 32189 funpartfv 32564 tailfb 32883 el3v23 34498 eldm4 34533 eldmcnv 34606 ecin0 34610 brcoss3 34681 pwslnmlem1 38442 rlimdmafv 42026 dfatsnafv2 42101 dfafv23 42102 dfatdmfcoafv2 42103 rlimdmafv2 42107 uspgrsprfo 42550 |
Copyright terms: Public domain | W3C validator |