Theorem el2v 3482

Description: If a proposition is implied by 𝑥 ∈ V and 𝑦 ∈ V (which is true, see vex 3478), 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

Step	Hyp	Ref	Expression
1		vex 3478	. 2 ⊢ 𝑥 ∈ V
2		vex 3478	. 2 ⊢ 𝑦 ∈ V
3		el2v.1	. 2 ⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) → 𝜑)
4	1, 2, 3	mp2an 690	1 ⊢ 𝜑

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  Vcvv 3474

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476

This theorem is referenced by:  codir  6121  dfco2  6244  1st2val  8002  2nd2val  8003  fnmap  8826  enrefnn  9046  unfi  9171  wemappo  9543  wemapsolem  9544  fin23lem26  10319  seqval  13976  hash2exprb  14431  hashle2prv  14438  mreexexlem4d  17590  pmtrrn2  19327  alexsubALTlem4  23553  elqaalem2  25832  upgrex  28349  cusgrsize  28708  erclwwlkref  29270  erclwwlksym  29271  erclwwlknref  29319  erclwwlknsym  29320  eclclwwlkn1  29325  gonanegoal  34338  gonarlem  34380  gonar  34381  fmla0disjsuc  34384  fmlasucdisj  34385  mclsppslem  34569  fneer  35233  curunc  36465  matunitlindflem2  36480  vvdifopab  37123  inxprnres  37156  ineccnvmo  37221  alrmomorn  37222  dfcoss2  37278  dfcoss3  37279  cosscnv  37281  cocossss  37301  cnvcosseq  37302  refressn  37308  antisymressn  37309  trressn  37310  rncossdmcoss  37320  symrelcoss3  37330  1cosscnvxrn  37340  cosscnvssid3  37341  cosscnvssid4  37342  coss0  37344  trcoss  37347  trcoss2  37349  erimeq2  37543  dfeldisj3  37584  dfeldisj4  37585  dfantisymrel5  37627  ismrc  41429  en2pr  42288  pr2cv  42289  ovnsubaddlem1  45276  sprsymrelfvlem  46148  sprsymrelf1lem  46149  prprelb  46174  prprspr2  46176  reuprpr  46181  2exopprim  46183  reuopreuprim  46184  c0snmgmhm  46703