Theorem el2v 3448

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2111  Vcvv 3441

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443

This theorem is referenced by:  codir  5947  dfco2  6065  1st2val  7699  2nd2val  7700  fnmap  8396  wemappo  8997  wemapsolem  8998  fin23lem26  9736  seqval  13375  hash2exprb  13825  hashle2prv  13832  mreexexlem4d  16910  pmtrrn2  18580  alexsubALTlem4  22655  elqaalem2  24916  upgrex  26885  cusgrsize  27244  erclwwlkref  27805  erclwwlksym  27806  erclwwlknref  27854  erclwwlknsym  27855  eclclwwlkn1  27860  gonanegoal  32712  gonarlem  32754  gonar  32755  fmla0disjsuc  32758  fmlasucdisj  32759  mclsppslem  32943  fneer  33814  curunc  35039  matunitlindflem2  35054  vvdifopab  35681  inxprnres  35709  ineccnvmo  35771  alrmomorn  35772  dfcoss2  35821  dfcoss3  35822  cocossss  35841  cnvcosseq  35842  rncossdmcoss  35855  symrelcoss3  35865  1cosscnvxrn  35875  cosscnvssid3  35876  cosscnvssid4  35877  coss0  35879  trcoss  35882  trcoss2  35884  erim2  36071  dfeldisj3  36112  dfeldisj4  36113  ismrc  39642  en2pr  40246  pr2cv  40247  ovnsubaddlem1  43209  sprsymrelfvlem  44007  sprsymrelf1lem  44008  prprelb  44033  prprspr2  44035  reuprpr  44040  2exopprim  44042  reuopreuprim  44043  c0snmgmhm  44538