Theorem el2v 3451

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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446

This theorem is referenced by:  codir  6081  dfco2  6206  1st2val  7975  2nd2val  7976  fnmap  8783  enrefnn  8995  unfi  9112  wemappo  9478  wemapsolem  9479  fin23lem26  10254  seqval  13953  hash2exprb  14412  hashle2prv  14419  hash3tpexb  14435  mreexexlem4d  17584  pmtrrn2  19366  c0snmgmhm  20347  alexsubALTlem4  23913  elqaalem2  26204  seqsval  28158  upgrex  28995  cusgrsize  29358  erclwwlkref  29922  erclwwlksym  29923  erclwwlknref  29971  erclwwlknsym  29972  eclclwwlkn1  29977  gonanegoal  35312  gonarlem  35354  gonar  35355  fmla0disjsuc  35358  fmlasucdisj  35359  mclsppslem  35543  fneer  36314  curunc  37569  matunitlindflem2  37584  vvdifopab  38222  inxprnres  38253  ineccnvmo  38312  alrmomorn  38313  dfcoss2  38377  dfcoss3  38378  cosscnv  38380  cocossss  38400  cnvcosseq  38401  refressn  38407  antisymressn  38408  trressn  38409  rncossdmcoss  38419  symrelcoss3  38429  1cosscnvxrn  38439  cosscnvssid3  38440  cosscnvssid4  38441  coss0  38443  trcoss  38446  trcoss2  38448  erimeq2  38643  dfeldisj3  38684  dfeldisj4  38685  dfantisymrel5  38727  ismrc  42662  en2pr  43509  pr2cv  43510  permaxext  44968  permac8prim  44977  ovnsubaddlem1  46541  sprsymrelfvlem  47464  sprsymrelf1lem  47465  prprelb  47490  prprspr2  47492  reuprpr  47497  2exopprim  47499  reuopreuprim  47500