Theorem el2v 3483

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107  Vcvv 3475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477

This theorem is referenced by:  codir  6122  dfco2  6245  1st2val  8003  2nd2val  8004  fnmap  8827  enrefnn  9047  unfi  9172  wemappo  9544  wemapsolem  9545  fin23lem26  10320  seqval  13977  hash2exprb  14432  hashle2prv  14439  mreexexlem4d  17591  pmtrrn2  19328  alexsubALTlem4  23554  elqaalem2  25833  upgrex  28352  cusgrsize  28711  erclwwlkref  29273  erclwwlksym  29274  erclwwlknref  29322  erclwwlknsym  29323  eclclwwlkn1  29328  gonanegoal  34343  gonarlem  34385  gonar  34386  fmla0disjsuc  34389  fmlasucdisj  34390  mclsppslem  34574  fneer  35238  curunc  36470  matunitlindflem2  36485  vvdifopab  37128  inxprnres  37161  ineccnvmo  37226  alrmomorn  37227  dfcoss2  37283  dfcoss3  37284  cosscnv  37286  cocossss  37306  cnvcosseq  37307  refressn  37313  antisymressn  37314  trressn  37315  rncossdmcoss  37325  symrelcoss3  37335  1cosscnvxrn  37345  cosscnvssid3  37346  cosscnvssid4  37347  coss0  37349  trcoss  37352  trcoss2  37354  erimeq2  37548  dfeldisj3  37589  dfeldisj4  37590  dfantisymrel5  37632  ismrc  41439  en2pr  42298  pr2cv  42299  ovnsubaddlem1  45286  sprsymrelfvlem  46158  sprsymrelf1lem  46159  prprelb  46184  prprspr2  46186  reuprpr  46191  2exopprim  46193  reuopreuprim  46194  c0snmgmhm  46713