![]() |
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 3448) and another antecedent, then it is implied by that other antecedent. Deduction associated with elv 3450. (Contributed by Peter Mazsa, 23-Oct-2018.) |
Ref | Expression |
---|---|
elvd.1 | ⊢ ((𝜑 ∧ 𝑥 ∈ V) → 𝜓) |
Ref | Expression |
---|---|
elvd | ⊢ (𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 3448 | . 2 ⊢ 𝑥 ∈ V | |
2 | elvd.1 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ V) → 𝜓) | |
3 | 1, 2 | mpan2 690 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∈ wcel 2107 Vcvv 3444 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2716 df-cleq 2730 df-clel 2816 df-v 3446 |
This theorem is referenced by: inimasn 6107 predep 6283 dffv3 6836 dmfco 6935 fsnex 7226 2ndconst 8026 curry1 8029 qsel 8694 ralxpmap 8793 domunsn 9030 dif1ennnALT 9180 eqinf 9379 dfacacn 10036 dfac13 10037 intgru 10709 shftfib 14917 rlimdm 15393 mat1scmat 21840 imasnopn 22993 imasncld 22994 imasncls 22995 ustuqtop1 23545 ustuqtop2 23546 ustuqtop3 23547 blval2 23870 dfnbgr2 28114 nbuhgr 28120 iunsnima2 31366 fmlasucdisj 33797 opelco3 34159 funpartfv 34462 tailfb 34781 el3v23 36615 eldm4 36666 eldmcnv 36738 ecin0 36745 brcoss3 36827 refressn 36837 disjlem19 37195 pwslnmlem1 41322 rlimdmafv 45304 dfatsnafv2 45379 dfafv23 45380 dfatdmfcoafv2 45381 rlimdmafv2 45385 uspgrsprfo 45945 |
Copyright terms: Public domain | W3C validator |