Theorem el2v 3447

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  Vcvv 3440

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442

This theorem is referenced by:  codir  6077  dfco2  6203  1st2val  7961  2nd2val  7962  fnmap  8770  enrefnn  8983  unfi  9095  wemappo  9454  wemapsolem  9455  fin23lem26  10235  seqval  13935  hash2exprb  14394  hashle2prv  14401  hash3tpexb  14417  mreexexlem4d  17570  pmtrrn2  19389  c0snmgmhm  20398  alexsubALTlem4  23994  elqaalem2  26284  seqsval  28284  upgrex  29165  cusgrsize  29528  erclwwlkref  30095  erclwwlksym  30096  erclwwlknref  30144  erclwwlknsym  30145  eclclwwlkn1  30150  gonanegoal  35546  gonarlem  35588  gonar  35589  fmla0disjsuc  35592  fmlasucdisj  35593  mclsppslem  35777  fneer  36547  curunc  37803  matunitlindflem2  37818  vvdifopab  38460  inxprnres  38493  ineccnvmo  38552  alrmomorn  38553  dfsucmap3  38647  dmsucmap  38652  dfcoss2  38686  dfcoss3  38687  cosscnv  38689  cocossss  38709  cnvcosseq  38710  refressn  38716  antisymressn  38717  trressn  38718  rncossdmcoss  38728  symrelcoss3  38738  1cosscnvxrn  38748  cosscnvssid3  38749  cosscnvssid4  38750  coss0  38752  trcoss  38755  trcoss2  38757  erimeq2  38947  dfeldisj3  38988  dfeldisj4  38989  dfantisymrel5  39031  ismrc  42953  en2pr  43798  pr2cv  43799  permaxext  45256  permac8prim  45265  ovnsubaddlem1  46824  sprsymrelfvlem  47746  sprsymrelf1lem  47747  prprelb  47772  prprspr2  47774  reuprpr  47779  2exopprim  47781  reuopreuprim  47782