Theorem el2v 3482

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  Vcvv 3474

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476

This theorem is referenced by:  codir  6121  dfco2  6244  1st2val  8005  2nd2val  8006  fnmap  8829  enrefnn  9049  unfi  9174  wemappo  9546  wemapsolem  9547  fin23lem26  10322  seqval  13979  hash2exprb  14434  hashle2prv  14441  mreexexlem4d  17593  pmtrrn2  19330  alexsubALTlem4  23561  elqaalem2  25840  upgrex  28390  cusgrsize  28749  erclwwlkref  29311  erclwwlksym  29312  erclwwlknref  29360  erclwwlknsym  29361  eclclwwlkn1  29366  gonanegoal  34412  gonarlem  34454  gonar  34455  fmla0disjsuc  34458  fmlasucdisj  34459  mclsppslem  34643  fneer  35330  curunc  36562  matunitlindflem2  36577  vvdifopab  37220  inxprnres  37253  ineccnvmo  37318  alrmomorn  37319  dfcoss2  37375  dfcoss3  37376  cosscnv  37378  cocossss  37398  cnvcosseq  37399  refressn  37405  antisymressn  37406  trressn  37407  rncossdmcoss  37417  symrelcoss3  37427  1cosscnvxrn  37437  cosscnvssid3  37438  cosscnvssid4  37439  coss0  37441  trcoss  37444  trcoss2  37446  erimeq2  37640  dfeldisj3  37681  dfeldisj4  37682  dfantisymrel5  37724  ismrc  41527  en2pr  42386  pr2cv  42387  ovnsubaddlem1  45371  sprsymrelfvlem  46243  sprsymrelf1lem  46244  prprelb  46269  prprspr2  46271  reuprpr  46276  2exopprim  46278  reuopreuprim  46279  c0snmgmhm  46798