Theorem el2v 3501

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

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

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 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-v 3496

This theorem is referenced by:  codir  5980  dfco2  6098  1st2val  7717  2nd2val  7718  fnmap  8413  wemappo  9013  wemapsolem  9014  fin23lem26  9747  seqval  13381  hash2exprb  13830  hashle2prv  13837  mreexexlem4d  16918  pmtrrn2  18588  alexsubALTlem4  22658  elqaalem2  24909  upgrex  26877  cusgrsize  27236  erclwwlkref  27798  erclwwlksym  27799  erclwwlknref  27848  erclwwlknsym  27849  eclclwwlkn1  27854  gonanegoal  32599  gonarlem  32641  gonar  32642  fmla0disjsuc  32645  fmlasucdisj  32646  mclsppslem  32830  fneer  33701  curunc  34889  matunitlindflem2  34904  vvdifopab  35536  inxprnres  35564  ineccnvmo  35626  alrmomorn  35627  dfcoss2  35676  dfcoss3  35677  cocossss  35696  cnvcosseq  35697  rncossdmcoss  35710  symrelcoss3  35720  1cosscnvxrn  35730  cosscnvssid3  35731  cosscnvssid4  35732  coss0  35734  trcoss  35737  trcoss2  35739  erim2  35926  dfeldisj3  35967  dfeldisj4  35968  ismrc  39318  en2pr  39926  pr2cv  39927  ovnsubaddlem1  42872  sprsymrelfvlem  43672  sprsymrelf1lem  43673  prprelb  43698  prprspr2  43700  reuprpr  43705  2exopprim  43707  reuopreuprim  43708  c0snmgmhm  44205