![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > el2v | Structured version Visualization version GIF version |
Description: If a proposition is implied by 𝑥 ∈ V and 𝑦 ∈ V (which is true, see vex 3401), then it is true. (Contributed by Peter Mazsa, 13-Oct-2018.) |
Ref | Expression |
---|---|
el2v.1 | ⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) → 𝜑) |
Ref | Expression |
---|---|
el2v | ⊢ 𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 3401 | . 2 ⊢ 𝑥 ∈ V | |
2 | vex 3401 | . 2 ⊢ 𝑦 ∈ V | |
3 | el2v.1 | . 2 ⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) → 𝜑) | |
4 | 1, 2, 3 | mp2an 682 | 1 ⊢ 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∈ wcel 2107 Vcvv 3398 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-12 2163 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-tru 1605 df-ex 1824 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-v 3400 |
This theorem is referenced by: vvdifopab 34664 inxprnres 34696 ineccnvmo 34755 alrmomorn 34756 dfcoss2 34804 dfcoss3 34805 cocossss 34824 cnvcosseq 34825 rncossdmcoss 34838 symrelcoss3 34848 1cosscnvxrn 34858 cosscnvssid3 34859 cosscnvssid4 34860 coss0 34862 trcoss 34865 trcoss2 34867 prprelb 42465 prprspr2 42467 |
Copyright terms: Public domain | W3C validator |