Theorem el2v 3454

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

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

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 3449

This theorem is referenced by:  codir  6093  dfco2  6218  1st2val  7996  2nd2val  7997  fnmap  8806  enrefnn  9018  unfi  9135  wemappo  9502  wemapsolem  9503  fin23lem26  10278  seqval  13977  hash2exprb  14436  hashle2prv  14443  hash3tpexb  14459  mreexexlem4d  17608  pmtrrn2  19390  c0snmgmhm  20371  alexsubALTlem4  23937  elqaalem2  26228  seqsval  28182  upgrex  29019  cusgrsize  29382  erclwwlkref  29949  erclwwlksym  29950  erclwwlknref  29998  erclwwlknsym  29999  eclclwwlkn1  30004  gonanegoal  35339  gonarlem  35381  gonar  35382  fmla0disjsuc  35385  fmlasucdisj  35386  mclsppslem  35570  fneer  36341  curunc  37596  matunitlindflem2  37611  vvdifopab  38249  inxprnres  38280  ineccnvmo  38339  alrmomorn  38340  dfcoss2  38404  dfcoss3  38405  cosscnv  38407  cocossss  38427  cnvcosseq  38428  refressn  38434  antisymressn  38435  trressn  38436  rncossdmcoss  38446  symrelcoss3  38456  1cosscnvxrn  38466  cosscnvssid3  38467  cosscnvssid4  38468  coss0  38470  trcoss  38473  trcoss2  38475  erimeq2  38670  dfeldisj3  38711  dfeldisj4  38712  dfantisymrel5  38754  ismrc  42689  en2pr  43536  pr2cv  43537  permaxext  44995  permac8prim  45004  ovnsubaddlem1  46568  sprsymrelfvlem  47491  sprsymrelf1lem  47492  prprelb  47517  prprspr2  47519  reuprpr  47524  2exopprim  47526  reuopreuprim  47527