Theorem el2v 3457

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

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452

This theorem is used by:  codir  6114  dfco2  6241  1st2val  8015  2nd2val  8016  fnmap  8833  enrefnn  9054  unfi  9166  wemappo  9522  wemapsolem  9523  fin23lem26  10328  seqval  14077  hash2exprb  14537  hashle2prv  14544  hash3tpexb  14560  mreexexlem4d  17736  pmtrrn2  19588  c0snmgmhm  20604  matunitlindflem2  22903  alexsubALTlem4  24277  elqaalem2  26553  seqsval  28554  upgrex  29550  cusgrsize  29915  erclwwlkref  30491  erclwwlksym  30492  erclwwlknref  30540  erclwwlknsym  30541  eclclwwlkn1  30546  onvfowev  35714  gonanegoal  35932  gonarlem  35974  gonar  35975  fmla0disjsuc  35978  fmlasucdisj  35979  mclsppslem  36163  fneer  36973  curunc  38357  findcard4  38464  vvdifopab  39014  inxprnres  39047  ineccnvmo  39106  alrmomorn  39107  dfsucmap3  39212  dmsucmap  39217  dfcoss2  39252  dfcoss3  39253  cosscnv  39255  cocossss  39275  cnvcosseq  39276  refressn  39282  antisymressn  39283  trressn  39284  rncossdmcoss  39294  symrelcoss3  39304  1cosscnvxrn  39314  cosscnvssid3  39315  cosscnvssid4  39316  coss0  39318  trcoss  39321  trcoss2  39323  erimeq2  39512  dfeldisj3  39560  dfeldisj4  39561  eldisjdmqsim  39566  dfantisymrel5  39614  dfpetparts2  39721  dfpeters2  39723  ismrc  43547  en2pr  44388  pr2cv  44389  permaxext  45829  permac8prim  45838  ovnsubaddlem1  47399  sprsymrelfvlem  48391  sprsymrelf1lem  48392  prprelb  48417  prprspr2  48419  reuprpr  48424  2exopprim  48426  reuopreuprim  48427