Theorem el2v 3458

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  Vcvv 3451

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453

This theorem is used by:  codir  6114  dfco2  6246  1st2val  8029  2nd2val  8030  fnmap  8853  enrefnn  9074  unfi  9186  wemappo  9543  wemapsolem  9544  fin23lem26  10403  seqval  14155  hash2exprb  14616  hashle2prv  14623  hash3tpexb  14639  mreexexlem4d  17821  pmtrrn2  19674  c0snmgmhm  20692  matunitlindflem2  22995  alexsubALTlem4  24369  elqaalem2  26643  seqsval  28674  upgrex  29670  cusgrsize  30035  erclwwlkref  30611  erclwwlksym  30612  erclwwlknref  30660  erclwwlknsym  30661  eclclwwlkn1  30666  onvfowev  35899  gonanegoal  36117  gonarlem  36159  gonar  36160  fmla0disjsuc  36163  fmlasucdisj  36164  mclsppslem  36348  fneer  37141  curunc  38525  findcard4  38632  vvdifopab  39197  inxprnres  39230  ineccnvmo  39289  alrmomorn  39290  dfsucmap3  39395  dmsucmap  39400  dfcoss2  39435  dfcoss3  39436  cosscnv  39438  cocossss  39458  cnvcosseq  39459  refressn  39465  antisymressn  39466  trressn  39467  rncossdmcoss  39477  symrelcoss3  39487  1cosscnvxrn  39497  cosscnvssid3  39498  cosscnvssid4  39499  coss0  39501  trcoss  39504  trcoss2  39506  erimeq2  39695  dfeldisj3  39743  dfeldisj4  39744  eldisjdmqsim  39749  dfantisymrel5  39797  dfpetparts2  39904  dfpeters2  39906  ismrc  43711  en2pr  44547  pr2cv  44548  permaxext  45994  permac8prim  46003  ovnsubaddlem1  47579  sprsymrelfvlem  48571  sprsymrelf1lem  48572  prprelb  48597  prprspr2  48599  reuprpr  48604  2exopprim  48606  reuopreuprim  48607