Theorem el2v 3443

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111  Vcvv 3436

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438

This theorem is referenced by:  codir  6066  dfco2  6192  1st2val  7949  2nd2val  7950  fnmap  8757  enrefnn  8968  unfi  9080  wemappo  9435  wemapsolem  9436  fin23lem26  10216  seqval  13919  hash2exprb  14378  hashle2prv  14385  hash3tpexb  14401  mreexexlem4d  17553  pmtrrn2  19372  c0snmgmhm  20380  alexsubALTlem4  23965  elqaalem2  26255  seqsval  28218  upgrex  29070  cusgrsize  29433  erclwwlkref  30000  erclwwlksym  30001  erclwwlknref  30049  erclwwlknsym  30050  eclclwwlkn1  30055  gonanegoal  35396  gonarlem  35438  gonar  35439  fmla0disjsuc  35442  fmlasucdisj  35443  mclsppslem  35627  fneer  36397  curunc  37652  matunitlindflem2  37667  vvdifopab  38307  inxprnres  38340  ineccnvmo  38399  alrmomorn  38400  dfsucmap3  38486  dmsucmap  38491  dfcoss2  38525  dfcoss3  38526  cosscnv  38528  cocossss  38548  cnvcosseq  38549  refressn  38555  antisymressn  38556  trressn  38557  rncossdmcoss  38567  symrelcoss3  38577  1cosscnvxrn  38587  cosscnvssid3  38588  cosscnvssid4  38589  coss0  38591  trcoss  38594  trcoss2  38596  erimeq2  38786  dfeldisj3  38827  dfeldisj4  38828  dfantisymrel5  38870  ismrc  42804  en2pr  43650  pr2cv  43651  permaxext  45108  permac8prim  45117  ovnsubaddlem1  46678  sprsymrelfvlem  47600  sprsymrelf1lem  47601  prprelb  47626  prprspr2  47628  reuprpr  47633  2exopprim  47635  reuopreuprim  47636