Theorem el2v 3464

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2145  Vcvv 3457

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459

This theorem is referenced by:  codir  6110  dfco2  6235  1st2val  8002  2nd2val  8003  fnmap  8818  enrefnn  9031  unfi  9143  wemappo  9499  wemapsolem  9500  fin23lem26  10297  seqval  14036  hash2exprb  14496  hashle2prv  14503  hash3tpexb  14519  mreexexlem4d  17691  pmtrrn2  19518  c0snmgmhm  20532  alexsubALTlem4  24164  elqaalem2  26438  seqsval  28435  upgrex  29347  cusgrsize  29709  erclwwlkref  30276  erclwwlksym  30277  erclwwlknref  30325  erclwwlknsym  30326  eclclwwlkn1  30331  onvfowev  35466  gonanegoal  35710  gonarlem  35752  gonar  35753  fmla0disjsuc  35756  fmlasucdisj  35757  mclsppslem  35941  fneer  36721  curunc  38108  matunitlindflem2  38123  vvdifopab  38771  inxprnres  38804  ineccnvmo  38863  alrmomorn  38864  dfsucmap3  38969  dmsucmap  38974  dfcoss2  39009  dfcoss3  39010  cosscnv  39012  cocossss  39032  cnvcosseq  39033  refressn  39039  antisymressn  39040  trressn  39041  rncossdmcoss  39051  symrelcoss3  39061  1cosscnvxrn  39071  cosscnvssid3  39072  cosscnvssid4  39073  coss0  39075  trcoss  39078  trcoss2  39080  erimeq2  39269  dfeldisj3  39317  dfeldisj4  39318  eldisjdmqsim  39323  dfantisymrel5  39371  dfpetparts2  39478  dfpeters2  39480  ismrc  43289  en2pr  44130  pr2cv  44131  permaxext  45573  permac8prim  45582  ovnsubaddlem1  47143  sprsymrelfvlem  48095  sprsymrelf1lem  48096  prprelb  48121  prprspr2  48123  reuprpr  48128  2exopprim  48130  reuopreuprim  48131