Theorem el2v 3466

Description: If a proposition is implied by 𝑥 ∈ V and 𝑦 ∈ V (which is true, see vex 3463), 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 3463	. 2 ⊢ 𝑥 ∈ V
2		vex 3463	. 2 ⊢ 𝑦 ∈ V
3		el2v.1	. 2 ⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) → 𝜑)
4	1, 2, 3	mp2an 692	1 ⊢ 𝜑

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  Vcvv 3459

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461

This theorem is referenced by:  codir  6109  dfco2  6234  1st2val  8014  2nd2val  8015  fnmap  8845  enrefnn  9059  unfi  9183  wemappo  9561  wemapsolem  9562  fin23lem26  10337  seqval  14028  hash2exprb  14487  hashle2prv  14494  hash3tpexb  14510  mreexexlem4d  17657  pmtrrn2  19439  c0snmgmhm  20420  alexsubALTlem4  23986  elqaalem2  26278  seqsval  28211  upgrex  29017  cusgrsize  29380  erclwwlkref  29947  erclwwlksym  29948  erclwwlknref  29996  erclwwlknsym  29997  eclclwwlkn1  30002  gonanegoal  35320  gonarlem  35362  gonar  35363  fmla0disjsuc  35366  fmlasucdisj  35367  mclsppslem  35551  fneer  36317  curunc  37572  matunitlindflem2  37587  vvdifopab  38224  inxprnres  38256  ineccnvmo  38321  alrmomorn  38322  dfcoss2  38377  dfcoss3  38378  cosscnv  38380  cocossss  38400  cnvcosseq  38401  refressn  38407  antisymressn  38408  trressn  38409  rncossdmcoss  38419  symrelcoss3  38429  1cosscnvxrn  38439  cosscnvssid3  38440  cosscnvssid4  38441  coss0  38443  trcoss  38446  trcoss2  38448  erimeq2  38642  dfeldisj3  38683  dfeldisj4  38684  dfantisymrel5  38726  ismrc  42671  en2pr  43518  pr2cv  43519  permaxext  44978  ovnsubaddlem1  46547  sprsymrelfvlem  47452  sprsymrelf1lem  47453  prprelb  47478  prprspr2  47480  reuprpr  47485  2exopprim  47487  reuopreuprim  47488