Theorem el2v 3464

Description: If a proposition is implied by 𝑥 ∈ V and 𝑦 ∈ V (which is true, see vex 3461), 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 3461	. 2 ⊢ 𝑥 ∈ V
2		vex 3461	. 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 2146  Vcvv 3457

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459

This theorem is used by:  codir  6122  dfco2  6248  1st2val  8020  2nd2val  8021  fnmap  8836  enrefnn  9050  unfi  9162  wemappo  9518  wemapsolem  9519  fin23lem26  10324  seqval  14068  hash2exprb  14528  hashle2prv  14535  hash3tpexb  14551  mreexexlem4d  17727  pmtrrn2  19576  c0snmgmhm  20592  alexsubALTlem4  24260  elqaalem2  26534  seqsval  28534  upgrex  29499  cusgrsize  29864  erclwwlkref  30440  erclwwlksym  30441  erclwwlknref  30489  erclwwlknsym  30490  eclclwwlkn1  30495  onvfowev  35659  gonanegoal  35883  gonarlem  35925  gonar  35926  fmla0disjsuc  35929  fmlasucdisj  35930  mclsppslem  36114  fneer  36923  curunc  38312  matunitlindflem2  38327  findcard4  38424  vvdifopab  38974  inxprnres  39007  ineccnvmo  39066  alrmomorn  39067  dfsucmap3  39172  dmsucmap  39177  dfcoss2  39212  dfcoss3  39213  cosscnv  39215  cocossss  39235  cnvcosseq  39236  refressn  39242  antisymressn  39243  trressn  39244  rncossdmcoss  39254  symrelcoss3  39264  1cosscnvxrn  39274  cosscnvssid3  39275  cosscnvssid4  39276  coss0  39278  trcoss  39281  trcoss2  39283  erimeq2  39472  dfeldisj3  39520  dfeldisj4  39521  eldisjdmqsim  39526  dfantisymrel5  39574  dfpetparts2  39681  dfpeters2  39683  ismrc  43492  en2pr  44333  pr2cv  44334  permaxext  45774  permac8prim  45783  ovnsubaddlem1  47344  sprsymrelfvlem  48299  sprsymrelf1lem  48300  prprelb  48325  prprspr2  48327  reuprpr  48332  2exopprim  48334  reuopreuprim  48335