|   | 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 3483) and another antecedent, then it is implied by that other antecedent. Deduction associated with elv 3484. (Contributed by Peter Mazsa, 23-Oct-2018.) | 
| Ref | Expression | 
|---|---|
| elvd.1 | ⊢ ((𝜑 ∧ 𝑥 ∈ V) → 𝜓) | 
| Ref | Expression | 
|---|---|
| elvd | ⊢ (𝜑 → 𝜓) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | vex 3483 | . 2 ⊢ 𝑥 ∈ V | |
| 2 | elvd.1 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ V) → 𝜓) | |
| 3 | 1, 2 | mpan2 691 | 1 ⊢ (𝜑 → 𝜓) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2107 Vcvv 3479 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1542 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-v 3481 | 
| This theorem is referenced by: inimasn 6175 predep 6350 dffv3 6901 dmfco 7004 fsnex 7304 2ndconst 8127 curry1 8130 qsel 8837 ralxpmap 8937 domunsn 9168 dif1ennnALT 9312 eqinf 9525 dfacacn 10183 dfac13 10184 intgru 10855 shftfib 15112 rlimdm 15588 mat1scmat 22546 imasnopn 23699 imasncld 23700 imasncls 23701 ustuqtop1 24251 ustuqtop2 24252 ustuqtop3 24253 blval2 24576 mulsval 28136 dfnbgr2 29355 nbuhgr 29361 iunsnima2 32632 gblacfnacd 35114 fmlasucdisj 35405 opelco3 35776 funpartfv 35947 tailfb 36379 el3v23 38230 eldm4 38276 eldmcnv 38347 ecin0 38354 brcoss3 38435 refressn 38445 disjlem19 38803 pwslnmlem1 43109 rlimdmafv 47194 dfatsnafv2 47269 dfafv23 47270 dfatdmfcoafv2 47271 rlimdmafv2 47275 dfclnbgr2 47815 uspgrsprfo 48069 | 
| Copyright terms: Public domain | W3C validator |