![]() |
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 3443) and another antecedent, then it is implied by that other antecedent. Deduction associated with elv 3445. (Contributed by Peter Mazsa, 23-Oct-2018.) |
Ref | Expression |
---|---|
elvd.1 | ⊢ ((𝜑 ∧ 𝑥 ∈ V) → 𝜓) |
Ref | Expression |
---|---|
elvd | ⊢ (𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 3443 | . 2 ⊢ 𝑥 ∈ V | |
2 | elvd.1 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ V) → 𝜓) | |
3 | 1, 2 | mpan2 687 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
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 |
Copyright terms: Public domain | W3C validator |