Theorem el2v 3451

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  Vcvv 3444

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446

This theorem is referenced by:  codir  6081  dfco2  6206  1st2val  7975  2nd2val  7976  fnmap  8783  enrefnn  8995  unfi  9112  wemappo  9478  wemapsolem  9479  fin23lem26  10254  seqval  13953  hash2exprb  14412  hashle2prv  14419  hash3tpexb  14435  mreexexlem4d  17588  pmtrrn2  19374  c0snmgmhm  20382  alexsubALTlem4  23970  elqaalem2  26261  seqsval  28222  upgrex  29072  cusgrsize  29435  erclwwlkref  29999  erclwwlksym  30000  erclwwlknref  30048  erclwwlknsym  30049  eclclwwlkn1  30054  gonanegoal  35332  gonarlem  35374  gonar  35375  fmla0disjsuc  35378  fmlasucdisj  35379  mclsppslem  35563  fneer  36334  curunc  37589  matunitlindflem2  37604  vvdifopab  38242  inxprnres  38273  ineccnvmo  38332  alrmomorn  38333  dfcoss2  38397  dfcoss3  38398  cosscnv  38400  cocossss  38420  cnvcosseq  38421  refressn  38427  antisymressn  38428  trressn  38429  rncossdmcoss  38439  symrelcoss3  38449  1cosscnvxrn  38459  cosscnvssid3  38460  cosscnvssid4  38461  coss0  38463  trcoss  38466  trcoss2  38468  erimeq2  38663  dfeldisj3  38704  dfeldisj4  38705  dfantisymrel5  38747  ismrc  42682  en2pr  43529  pr2cv  43530  permaxext  44988  permac8prim  44997  ovnsubaddlem1  46561  sprsymrelfvlem  47484  sprsymrelf1lem  47485  prprelb  47510  prprspr2  47512  reuprpr  47517  2exopprim  47519  reuopreuprim  47520