![]() |
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 3475), 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 3475 | . 2 ⊢ 𝑥 ∈ V | |
2 | vex 3475 | . 2 ⊢ 𝑦 ∈ V | |
3 | el2v.1 | . 2 ⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) → 𝜑) | |
4 | 1, 2, 3 | mp2an 690 | 1 ⊢ 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∈ wcel 2098 Vcvv 3471 |
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 2698 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2705 df-cleq 2719 df-clel 2805 df-v 3473 |
This theorem is referenced by: codir 6129 dfco2 6252 1st2val 8025 2nd2val 8026 fnmap 8856 enrefnn 9076 unfi 9201 wemappo 9578 wemapsolem 9579 fin23lem26 10354 seqval 14015 hash2exprb 14470 hashle2prv 14477 mreexexlem4d 17632 pmtrrn2 19420 c0snmgmhm 20406 alexsubALTlem4 23972 elqaalem2 26273 seqsval 28179 upgrex 28923 cusgrsize 29286 erclwwlkref 29848 erclwwlksym 29849 erclwwlknref 29897 erclwwlknsym 29898 eclclwwlkn1 29903 gonanegoal 34967 gonarlem 35009 gonar 35010 fmla0disjsuc 35013 fmlasucdisj 35014 mclsppslem 35198 fneer 35842 curunc 37080 matunitlindflem2 37095 vvdifopab 37736 inxprnres 37768 ineccnvmo 37833 alrmomorn 37834 dfcoss2 37889 dfcoss3 37890 cosscnv 37892 cocossss 37912 cnvcosseq 37913 refressn 37919 antisymressn 37920 trressn 37921 rncossdmcoss 37931 symrelcoss3 37941 1cosscnvxrn 37951 cosscnvssid3 37952 cosscnvssid4 37953 coss0 37955 trcoss 37958 trcoss2 37960 erimeq2 38154 dfeldisj3 38195 dfeldisj4 38196 dfantisymrel5 38238 ismrc 42124 en2pr 42980 pr2cv 42981 ovnsubaddlem1 45960 sprsymrelfvlem 46832 sprsymrelf1lem 46833 prprelb 46858 prprspr2 46860 reuprpr 46865 2exopprim 46867 reuopreuprim 46868 |
Copyright terms: Public domain | W3C validator |