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  8016  2nd2val  8017  fnmap  8847  enrefnn  9061  unfi  9185  wemappo  9563  wemapsolem  9564  fin23lem26  10339  seqval  14030  hash2exprb  14489  hashle2prv  14496  hash3tpexb  14512  mreexexlem4d  17659  pmtrrn2  19441  c0snmgmhm  20422  alexsubALTlem4  23988  elqaalem2  26280  seqsval  28234  upgrex  29071  cusgrsize  29434  erclwwlkref  30001  erclwwlksym  30002  erclwwlknref  30050  erclwwlknsym  30051  eclclwwlkn1  30056  gonanegoal  35374  gonarlem  35416  gonar  35417  fmla0disjsuc  35420  fmlasucdisj  35421  mclsppslem  35605  fneer  36371  curunc  37626  matunitlindflem2  37641  vvdifopab  38278  inxprnres  38310  ineccnvmo  38375  alrmomorn  38376  dfcoss2  38431  dfcoss3  38432  cosscnv  38434  cocossss  38454  cnvcosseq  38455  refressn  38461  antisymressn  38462  trressn  38463  rncossdmcoss  38473  symrelcoss3  38483  1cosscnvxrn  38493  cosscnvssid3  38494  cosscnvssid4  38495  coss0  38497  trcoss  38500  trcoss2  38502  erimeq2  38696  dfeldisj3  38737  dfeldisj4  38738  dfantisymrel5  38780  ismrc  42724  en2pr  43571  pr2cv  43572  permaxext  45030  ovnsubaddlem1  46599  sprsymrelfvlem  47504  sprsymrelf1lem  47505  prprelb  47530  prprspr2  47532  reuprpr  47537  2exopprim  47539  reuopreuprim  47540