Theorem el2v 3503

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2114  Vcvv 3496

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-v 3498

This theorem is referenced by:  codir  5982  dfco2  6100  1st2val  7719  2nd2val  7720  fnmap  8415  wemappo  9015  wemapsolem  9016  fin23lem26  9749  seqval  13383  hash2exprb  13832  hashle2prv  13839  mreexexlem4d  16920  pmtrrn2  18590  alexsubALTlem4  22660  elqaalem2  24911  upgrex  26879  cusgrsize  27238  erclwwlkref  27800  erclwwlksym  27801  erclwwlknref  27850  erclwwlknsym  27851  eclclwwlkn1  27856  gonanegoal  32601  gonarlem  32643  gonar  32644  fmla0disjsuc  32647  fmlasucdisj  32648  mclsppslem  32832  fneer  33703  curunc  34876  matunitlindflem2  34891  vvdifopab  35523  inxprnres  35551  ineccnvmo  35613  alrmomorn  35614  dfcoss2  35663  dfcoss3  35664  cocossss  35683  cnvcosseq  35684  rncossdmcoss  35697  symrelcoss3  35707  1cosscnvxrn  35717  cosscnvssid3  35718  cosscnvssid4  35719  coss0  35721  trcoss  35724  trcoss2  35726  erim2  35913  dfeldisj3  35954  dfeldisj4  35955  ismrc  39305  en2pr  39913  pr2cv  39914  ovnsubaddlem1  42859  sprsymrelfvlem  43659  sprsymrelf1lem  43660  prprelb  43685  prprspr2  43687  reuprpr  43692  2exopprim  43694  reuopreuprim  43695  c0snmgmhm  44192