Theorem el2v 3479

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.)

Hypothesis

Ref	Expression
el2v.1	⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) → 𝜑)

Assertion

Ref	Expression
el2v	⊢ 𝜑

Proof of Theorem 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 ⊢ 𝜑

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