Theorem el2v 3457

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

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

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452

This theorem is referenced by:  codir  6096  dfco2  6221  1st2val  7999  2nd2val  8000  fnmap  8809  enrefnn  9021  unfi  9141  wemappo  9509  wemapsolem  9510  fin23lem26  10285  seqval  13984  hash2exprb  14443  hashle2prv  14450  hash3tpexb  14466  mreexexlem4d  17615  pmtrrn2  19397  c0snmgmhm  20378  alexsubALTlem4  23944  elqaalem2  26235  seqsval  28189  upgrex  29026  cusgrsize  29389  erclwwlkref  29956  erclwwlksym  29957  erclwwlknref  30005  erclwwlknsym  30006  eclclwwlkn1  30011  gonanegoal  35346  gonarlem  35388  gonar  35389  fmla0disjsuc  35392  fmlasucdisj  35393  mclsppslem  35577  fneer  36348  curunc  37603  matunitlindflem2  37618  vvdifopab  38256  inxprnres  38287  ineccnvmo  38346  alrmomorn  38347  dfcoss2  38411  dfcoss3  38412  cosscnv  38414  cocossss  38434  cnvcosseq  38435  refressn  38441  antisymressn  38442  trressn  38443  rncossdmcoss  38453  symrelcoss3  38463  1cosscnvxrn  38473  cosscnvssid3  38474  cosscnvssid4  38475  coss0  38477  trcoss  38480  trcoss2  38482  erimeq2  38677  dfeldisj3  38718  dfeldisj4  38719  dfantisymrel5  38761  ismrc  42696  en2pr  43543  pr2cv  43544  permaxext  45002  permac8prim  45011  ovnsubaddlem1  46575  sprsymrelfvlem  47495  sprsymrelf1lem  47496  prprelb  47521  prprspr2  47523  reuprpr  47528  2exopprim  47530  reuopreuprim  47531