Theorem el2v 3436

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  Vcvv 3429

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431

This theorem is referenced by:  codir  6083  dfco2  6209  1st2val  7970  2nd2val  7971  fnmap  8780  enrefnn  8993  unfi  9105  wemappo  9464  wemapsolem  9465  fin23lem26  10247  seqval  13974  hash2exprb  14433  hashle2prv  14440  hash3tpexb  14456  mreexexlem4d  17613  pmtrrn2  19435  c0snmgmhm  20442  alexsubALTlem4  24015  elqaalem2  26286  seqsval  28280  upgrex  29161  cusgrsize  29523  erclwwlkref  30090  erclwwlksym  30091  erclwwlknref  30139  erclwwlknsym  30140  eclclwwlkn1  30145  gonanegoal  35534  gonarlem  35576  gonar  35577  fmla0disjsuc  35580  fmlasucdisj  35581  mclsppslem  35765  fneer  36535  curunc  37923  matunitlindflem2  37938  vvdifopab  38586  inxprnres  38619  ineccnvmo  38678  alrmomorn  38679  dfsucmap3  38784  dmsucmap  38789  dfcoss2  38824  dfcoss3  38825  cosscnv  38827  cocossss  38847  cnvcosseq  38848  refressn  38854  antisymressn  38855  trressn  38856  rncossdmcoss  38866  symrelcoss3  38876  1cosscnvxrn  38886  cosscnvssid3  38887  cosscnvssid4  38888  coss0  38890  trcoss  38893  trcoss2  38895  erimeq2  39084  dfeldisj3  39132  dfeldisj4  39133  eldisjdmqsim  39138  dfantisymrel5  39186  dfpetparts2  39293  dfpeters2  39295  ismrc  43133  en2pr  43974  pr2cv  43975  permaxext  45432  permac8prim  45441  ovnsubaddlem1  46998  sprsymrelfvlem  47950  sprsymrelf1lem  47951  prprelb  47976  prprspr2  47978  reuprpr  47983  2exopprim  47985  reuopreuprim  47986