![]() |
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 3465) and another antecedent, then it is implied by that other antecedent. Deduction associated with elv 3467. (Contributed by Peter Mazsa, 23-Oct-2018.) |
Ref | Expression |
---|---|
elvd.1 | ⊢ ((𝜑 ∧ 𝑥 ∈ V) → 𝜓) |
Ref | Expression |
---|---|
elvd | ⊢ (𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 3465 | . 2 ⊢ 𝑥 ∈ V | |
2 | elvd.1 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ V) → 𝜓) | |
3 | 1, 2 | mpan2 689 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∈ wcel 2098 Vcvv 3461 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-v 3463 |
This theorem is referenced by: inimasn 6162 predep 6338 dffv3 6892 dmfco 6993 fsnex 7292 2ndconst 8106 curry1 8109 qsel 8815 ralxpmap 8915 domunsn 9152 dif1ennnALT 9302 eqinf 9509 dfacacn 10166 dfac13 10167 intgru 10839 shftfib 15055 rlimdm 15531 mat1scmat 22485 imasnopn 23638 imasncld 23639 imasncls 23640 ustuqtop1 24190 ustuqtop2 24191 ustuqtop3 24192 blval2 24515 mulsval 28059 dfnbgr2 29222 nbuhgr 29228 iunsnima2 32488 fmlasucdisj 35140 opelco3 35501 funpartfv 35672 tailfb 35992 el3v23 37828 eldm4 37876 eldmcnv 37947 ecin0 37954 brcoss3 38035 refressn 38045 disjlem19 38403 pwslnmlem1 42658 rlimdmafv 46695 dfatsnafv2 46770 dfafv23 46771 dfatdmfcoafv2 46772 rlimdmafv2 46776 dfclnbgr2 47300 uspgrsprfo 47396 |
Copyright terms: Public domain | W3C validator |