Theorem el2v 3462

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143  Vcvv 3455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457

This theorem is referenced by:  codir  6120  dfco2  6246  1st2val  8010  2nd2val  8011  fnmap  8826  enrefnn  9039  unfi  9151  wemappo  9507  wemapsolem  9508  fin23lem26  10304  seqval  14044  hash2exprb  14504  hashle2prv  14511  hash3tpexb  14527  mreexexlem4d  17698  pmtrrn2  19525  c0snmgmhm  20540  alexsubALTlem4  24207  elqaalem2  26481  seqsval  28481  upgrex  29442  cusgrsize  29804  erclwwlkref  30371  erclwwlksym  30372  erclwwlknref  30420  erclwwlknsym  30421  eclclwwlkn1  30426  onvfowev  35600  gonanegoal  35844  gonarlem  35886  gonar  35887  fmla0disjsuc  35890  fmlasucdisj  35891  mclsppslem  36075  fneer  36884  curunc  38273  matunitlindflem2  38288  vvdifopab  38934  inxprnres  38967  ineccnvmo  39026  alrmomorn  39027  dfsucmap3  39132  dmsucmap  39137  dfcoss2  39172  dfcoss3  39173  cosscnv  39175  cocossss  39195  cnvcosseq  39196  refressn  39202  antisymressn  39203  trressn  39204  rncossdmcoss  39214  symrelcoss3  39224  1cosscnvxrn  39234  cosscnvssid3  39235  cosscnvssid4  39236  coss0  39238  trcoss  39241  trcoss2  39243  erimeq2  39432  dfeldisj3  39480  dfeldisj4  39481  eldisjdmqsim  39486  dfantisymrel5  39534  dfpetparts2  39641  dfpeters2  39643  ismrc  43452  en2pr  44293  pr2cv  44294  permaxext  45734  permac8prim  45743  ovnsubaddlem1  47304  sprsymrelfvlem  48259  sprsymrelf1lem  48260  prprelb  48285  prprspr2  48287  reuprpr  48292  2exopprim  48294  reuopreuprim  48295