Theorem el2v 3461

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2142  Vcvv 3454

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456

This theorem is referenced by:  codir  6107  dfco2  6232  1st2val  7998  2nd2val  7999  fnmap  8814  enrefnn  9027  unfi  9139  wemappo  9497  wemapsolem  9498  fin23lem26  10282  seqval  14025  hash2exprb  14484  hashle2prv  14491  hash3tpexb  14507  mreexexlem4d  17679  pmtrrn2  19500  c0snmgmhm  20511  alexsubALTlem4  24110  elqaalem2  26384  seqsval  28381  upgrex  29293  cusgrsize  29655  erclwwlkref  30222  erclwwlksym  30223  erclwwlknref  30271  erclwwlknsym  30272  eclclwwlkn1  30277  onvfowev  35459  gonanegoal  35702  gonarlem  35744  gonar  35745  fmla0disjsuc  35748  fmlasucdisj  35749  mclsppslem  35933  fneer  36713  curunc  38101  matunitlindflem2  38116  vvdifopab  38764  inxprnres  38797  ineccnvmo  38856  alrmomorn  38857  dfsucmap3  38962  dmsucmap  38967  dfcoss2  39002  dfcoss3  39003  cosscnv  39005  cocossss  39025  cnvcosseq  39026  refressn  39032  antisymressn  39033  trressn  39034  rncossdmcoss  39044  symrelcoss3  39054  1cosscnvxrn  39064  cosscnvssid3  39065  cosscnvssid4  39066  coss0  39068  trcoss  39071  trcoss2  39073  erimeq2  39262  dfeldisj3  39310  dfeldisj4  39311  eldisjdmqsim  39316  dfantisymrel5  39364  dfpetparts2  39471  dfpeters2  39473  ismrc  43282  en2pr  44123  pr2cv  44124  permaxext  45581  permac8prim  45590  ovnsubaddlem1  47144  sprsymrelfvlem  48096  sprsymrelf1lem  48097  prprelb  48122  prprspr2  48124  reuprpr  48129  2exopprim  48131  reuopreuprim  48132