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 705	1 ⊢ 𝜑

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456

This theorem is used by:  codir  6132  dfco2  6265  1st2val  8063  2nd2val  8064  fnmap  8891  enrefnn  9112  unfi  9224  wemappo  9580  wemapsolem  9581  fin23lem26  10442  seqval  14195  hash2exprb  14657  hashle2prv  14664  hash3tpexb  14680  mreexexlem4d  17871  pmtrrn2  19725  c0snmgmhm  20743  matunitlindflem2  23050  alexsubALTlem4  24424  elqaalem2  26700  seqsval  28731  upgrex  29727  cusgrsize  30092  erclwwlkref  30668  erclwwlksym  30669  erclwwlknref  30717  erclwwlknsym  30718  eclclwwlkn1  30723  onvfowev  36091  gonanegoal  36325  gonarlem  36367  gonar  36368  fmla0disjsuc  36371  fmlasucdisj  36372  mclsppslem  36556  fneer  37356  curunc  38793  findcard4  38900  vvdifopab  39463  inxprnres  39496  ineccnvmo  39555  alrmomorn  39556  dfsucmap3  39661  dmsucmap  39666  dfcoss2  39701  dfcoss3  39702  cosscnv  39704  cocossss  39724  cnvcosseq  39725  refressn  39731  antisymressn  39732  trressn  39733  rncossdmcoss  39743  symrelcoss3  39753  1cosscnvxrn  39763  cosscnvssid3  39764  cosscnvssid4  39765  coss0  39767  trcoss  39770  trcoss2  39772  erimeq2  39961  dfeldisj3  40009  dfeldisj4  40010  eldisjdmqsim  40015  dfantisymrel5  40063  dfpetparts2  40170  dfpeters2  40172  ismrc  43978  en2pr  44809  pr2cv  44810  permaxext  46259  permac8prim  46268  ovnsubaddlem1  47853  sprsymrelfvlem  48845  sprsymrelf1lem  48846  prprelb  48871  prprspr2  48873  reuprpr  48878  2exopprim  48880  reuopreuprim  48881