Theorem el2v 3443

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

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

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 3438

This theorem is referenced by:  codir  6069  dfco2  6194  1st2val  7952  2nd2val  7953  fnmap  8760  enrefnn  8972  unfi  9085  wemappo  9441  wemapsolem  9442  fin23lem26  10219  seqval  13919  hash2exprb  14378  hashle2prv  14385  hash3tpexb  14401  mreexexlem4d  17553  pmtrrn2  19339  c0snmgmhm  20347  alexsubALTlem4  23935  elqaalem2  26226  seqsval  28187  upgrex  29037  cusgrsize  29400  erclwwlkref  29964  erclwwlksym  29965  erclwwlknref  30013  erclwwlknsym  30014  eclclwwlkn1  30019  gonanegoal  35329  gonarlem  35371  gonar  35372  fmla0disjsuc  35375  fmlasucdisj  35376  mclsppslem  35560  fneer  36331  curunc  37586  matunitlindflem2  37601  vvdifopab  38239  inxprnres  38270  ineccnvmo  38329  alrmomorn  38330  dfcoss2  38394  dfcoss3  38395  cosscnv  38397  cocossss  38417  cnvcosseq  38418  refressn  38424  antisymressn  38425  trressn  38426  rncossdmcoss  38436  symrelcoss3  38446  1cosscnvxrn  38456  cosscnvssid3  38457  cosscnvssid4  38458  coss0  38460  trcoss  38463  trcoss2  38465  erimeq2  38660  dfeldisj3  38701  dfeldisj4  38702  dfantisymrel5  38744  ismrc  42678  en2pr  43524  pr2cv  43525  permaxext  44983  permac8prim  44992  ovnsubaddlem1  46555  sprsymrelfvlem  47478  sprsymrelf1lem  47479  prprelb  47504  prprspr2  47506  reuprpr  47511  2exopprim  47513  reuopreuprim  47514