MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  el2v Structured version   Visualization version   GIF version

Theorem el2v 3500
Description: If a proposition is implied by 𝑥 ∈ V and 𝑦 ∈ V (which is true, see vex 3496), then it is true. (Contributed by Peter Mazsa, 13-Oct-2018.)
Hypothesis
Ref Expression
el2v.1 ((𝑥 ∈ V ∧ 𝑦 ∈ V) → 𝜑)
Assertion
Ref Expression
el2v 𝜑

Proof of Theorem el2v
StepHypRef Expression
1 vex 3496 . 2 𝑥 ∈ V
2 vex 3496 . 2 𝑦 ∈ V
3 el2v.1 . 2 ((𝑥 ∈ V ∧ 𝑦 ∈ V) → 𝜑)
41, 2, 3mp2an 690 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398  wcel 2107  Vcvv 3493
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 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1774  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-v 3495
This theorem is referenced by:  codir  5973  dfco2  6091  1st2val  7709  2nd2val  7710  fnmap  8405  wemappo  9005  wemapsolem  9006  fin23lem26  9739  seqval  13372  hash2exprb  13821  hashle2prv  13828  mreexexlem4d  16910  pmtrrn2  18580  alexsubALTlem4  22650  elqaalem2  24901  upgrex  26869  cusgrsize  27228  erclwwlkref  27790  erclwwlksym  27791  erclwwlknref  27840  erclwwlknsym  27841  eclclwwlkn1  27846  gonanegoal  32587  gonarlem  32629  gonar  32630  fmla0disjsuc  32633  fmlasucdisj  32634  mclsppslem  32818  fneer  33689  curunc  34861  matunitlindflem2  34876  vvdifopab  35508  inxprnres  35536  ineccnvmo  35598  alrmomorn  35599  dfcoss2  35648  dfcoss3  35649  cocossss  35668  cnvcosseq  35669  rncossdmcoss  35682  symrelcoss3  35692  1cosscnvxrn  35702  cosscnvssid3  35703  cosscnvssid4  35704  coss0  35706  trcoss  35709  trcoss2  35711  erim2  35898  dfeldisj3  35939  dfeldisj4  35940  ismrc  39283  en2pr  39891  pr2cv  39892  ovnsubaddlem1  42837  sprsymrelfvlem  43637  sprsymrelf1lem  43638  prprelb  43663  prprspr2  43665  reuprpr  43670  2exopprim  43672  reuopreuprim  43673  c0snmgmhm  44170
  Copyright terms: Public domain W3C validator