Theorem el2v 3438

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  Vcvv 3430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3432

This theorem is referenced by:  codir  6022  dfco2  6146  1st2val  7845  2nd2val  7846  fnmap  8596  enrefnn  8807  unfi  8920  wemappo  9269  wemapsolem  9270  fin23lem26  10065  seqval  13713  hash2exprb  14166  hashle2prv  14173  mreexexlem4d  17337  pmtrrn2  19049  alexsubALTlem4  23182  elqaalem2  25461  upgrex  27443  cusgrsize  27802  erclwwlkref  28363  erclwwlksym  28364  erclwwlknref  28412  erclwwlknsym  28413  eclclwwlkn1  28418  gonanegoal  33293  gonarlem  33335  gonar  33336  fmla0disjsuc  33339  fmlasucdisj  33340  mclsppslem  33524  fneer  34521  curunc  35738  matunitlindflem2  35753  vvdifopab  36378  inxprnres  36406  ineccnvmo  36468  alrmomorn  36469  dfcoss2  36518  dfcoss3  36519  cocossss  36538  cnvcosseq  36539  rncossdmcoss  36552  symrelcoss3  36562  1cosscnvxrn  36572  cosscnvssid3  36573  cosscnvssid4  36574  coss0  36576  trcoss  36579  trcoss2  36581  erim2  36768  dfeldisj3  36809  dfeldisj4  36810  ismrc  40503  en2pr  41107  pr2cv  41108  ovnsubaddlem1  44062  sprsymrelfvlem  44894  sprsymrelf1lem  44895  prprelb  44920  prprspr2  44922  reuprpr  44927  2exopprim  44929  reuopreuprim  44930  c0snmgmhm  45424