Theorem el2v 3484

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105  Vcvv 3477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479

This theorem is referenced by:  codir  6142  dfco2  6266  1st2val  8040  2nd2val  8041  fnmap  8871  enrefnn  9085  unfi  9209  wemappo  9586  wemapsolem  9587  fin23lem26  10362  seqval  14049  hash2exprb  14506  hashle2prv  14513  hash3tpexb  14529  mreexexlem4d  17691  pmtrrn2  19492  c0snmgmhm  20478  alexsubALTlem4  24073  elqaalem2  26376  seqsval  28308  upgrex  29123  cusgrsize  29486  erclwwlkref  30048  erclwwlksym  30049  erclwwlknref  30097  erclwwlknsym  30098  eclclwwlkn1  30103  gonanegoal  35336  gonarlem  35378  gonar  35379  fmla0disjsuc  35382  fmlasucdisj  35383  mclsppslem  35567  fneer  36335  curunc  37588  matunitlindflem2  37603  vvdifopab  38241  inxprnres  38273  ineccnvmo  38338  alrmomorn  38339  dfcoss2  38394  dfcoss3  38395  cosscnv  38397  cocossss  38417  cnvcosseq  38418  refressn  38424  antisymressn  38425  trressn  38426  rncossdmcoss  38436  symrelcoss3  38446  1cosscnvxrn  38456  cosscnvssid3  38457  cosscnvssid4  38458  coss0  38460  trcoss  38463  trcoss2  38465  erimeq2  38659  dfeldisj3  38700  dfeldisj4  38701  dfantisymrel5  38743  ismrc  42688  en2pr  43536  pr2cv  43537  ovnsubaddlem1  46525  sprsymrelfvlem  47414  sprsymrelf1lem  47415  prprelb  47440  prprspr2  47442  reuprpr  47447  2exopprim  47449  reuopreuprim  47450