Theorem el2v 3438

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119  Vcvv 3431

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433

This theorem is referenced by:  codir  6070  dfco2  6196  1st2val  7959  2nd2val  7960  fnmap  8770  enrefnn  8983  unfi  9095  wemappo  9454  wemapsolem  9455  fin23lem26  10238  seqval  13965  hash2exprb  14424  hashle2prv  14431  hash3tpexb  14447  mreexexlem4d  17604  pmtrrn2  19426  c0snmgmhm  20433  alexsubALTlem4  24033  elqaalem2  26304  seqsval  28298  upgrex  29179  cusgrsize  29541  erclwwlkref  30108  erclwwlksym  30109  erclwwlknref  30157  erclwwlknsym  30158  eclclwwlkn1  30163  gonanegoal  35580  gonarlem  35622  gonar  35623  fmla0disjsuc  35626  fmlasucdisj  35627  mclsppslem  35811  fneer  36581  curunc  37969  matunitlindflem2  37984  vvdifopab  38632  inxprnres  38665  ineccnvmo  38724  alrmomorn  38725  dfsucmap3  38830  dmsucmap  38835  dfcoss2  38870  dfcoss3  38871  cosscnv  38873  cocossss  38893  cnvcosseq  38894  refressn  38900  antisymressn  38901  trressn  38902  rncossdmcoss  38912  symrelcoss3  38922  1cosscnvxrn  38932  cosscnvssid3  38933  cosscnvssid4  38934  coss0  38936  trcoss  38939  trcoss2  38941  erimeq2  39130  dfeldisj3  39178  dfeldisj4  39179  eldisjdmqsim  39184  dfantisymrel5  39232  dfpetparts2  39339  dfpeters2  39341  ismrc  43150  en2pr  43991  pr2cv  43992  permaxext  45449  permac8prim  45458  ovnsubaddlem1  47013  sprsymrelfvlem  47965  sprsymrelf1lem  47966  prprelb  47991  prprspr2  47993  reuprpr  47998  2exopprim  48000  reuopreuprim  48001