Theorem el2v 3445

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  Vcvv 3438

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 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440

This theorem is referenced by:  codir  6075  dfco2  6201  1st2val  7959  2nd2val  7960  fnmap  8768  enrefnn  8981  unfi  9093  wemappo  9452  wemapsolem  9453  fin23lem26  10233  seqval  13933  hash2exprb  14392  hashle2prv  14399  hash3tpexb  14415  mreexexlem4d  17568  pmtrrn2  19387  c0snmgmhm  20396  alexsubALTlem4  23992  elqaalem2  26282  seqsval  28249  upgrex  29114  cusgrsize  29477  erclwwlkref  30044  erclwwlksym  30045  erclwwlknref  30093  erclwwlknsym  30094  eclclwwlkn1  30099  gonanegoal  35495  gonarlem  35537  gonar  35538  fmla0disjsuc  35541  fmlasucdisj  35542  mclsppslem  35726  fneer  36496  curunc  37742  matunitlindflem2  37757  vvdifopab  38397  inxprnres  38430  ineccnvmo  38489  alrmomorn  38490  dfsucmap3  38576  dmsucmap  38581  dfcoss2  38615  dfcoss3  38616  cosscnv  38618  cocossss  38638  cnvcosseq  38639  refressn  38645  antisymressn  38646  trressn  38647  rncossdmcoss  38657  symrelcoss3  38667  1cosscnvxrn  38677  cosscnvssid3  38678  cosscnvssid4  38679  coss0  38681  trcoss  38684  trcoss2  38686  erimeq2  38876  dfeldisj3  38917  dfeldisj4  38918  dfantisymrel5  38960  ismrc  42885  en2pr  43730  pr2cv  43731  permaxext  45188  permac8prim  45197  ovnsubaddlem1  46756  sprsymrelfvlem  47678  sprsymrelf1lem  47679  prprelb  47704  prprspr2  47706  reuprpr  47711  2exopprim  47713  reuopreuprim  47714