Theorem el2v 3445

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2104  Vcvv 3437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3439

This theorem is referenced by:  codir  6040  dfco2  6163  1st2val  7891  2nd2val  7892  fnmap  8653  enrefnn  8872  unfi  8993  wemappo  9352  wemapsolem  9353  fin23lem26  10127  seqval  13778  hash2exprb  14230  hashle2prv  14237  mreexexlem4d  17401  pmtrrn2  19113  alexsubALTlem4  23246  elqaalem2  25525  upgrex  27507  cusgrsize  27866  erclwwlkref  28429  erclwwlksym  28430  erclwwlknref  28478  erclwwlknsym  28479  eclclwwlkn1  28484  gonanegoal  33359  gonarlem  33401  gonar  33402  fmla0disjsuc  33405  fmlasucdisj  33406  mclsppslem  33590  fneer  34587  curunc  35803  matunitlindflem2  35818  vvdifopab  36442  inxprnres  36470  ineccnvmo  36531  alrmomorn  36532  dfcoss2  36581  dfcoss3  36582  cocossss  36601  cnvcosseq  36602  rncossdmcoss  36615  symrelcoss3  36625  1cosscnvxrn  36635  cosscnvssid3  36636  cosscnvssid4  36637  coss0  36639  trcoss  36642  trcoss2  36644  erim2  36831  dfeldisj3  36872  dfeldisj4  36873  ismrc  40560  en2pr  41192  pr2cv  41193  ovnsubaddlem1  44158  sprsymrelfvlem  45000  sprsymrelf1lem  45001  prprelb  45026  prprspr2  45028  reuprpr  45033  2exopprim  45035  reuopreuprim  45036  c0snmgmhm  45530