Theorem el2v 3437

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  Vcvv 3430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432

This theorem is referenced by:  codir  6078  dfco2  6204  1st2val  7964  2nd2val  7965  fnmap  8774  enrefnn  8987  unfi  9099  wemappo  9458  wemapsolem  9459  fin23lem26  10241  seqval  13968  hash2exprb  14427  hashle2prv  14434  hash3tpexb  14450  mreexexlem4d  17607  pmtrrn2  19429  c0snmgmhm  20436  alexsubALTlem4  24028  elqaalem2  26300  seqsval  28297  upgrex  29178  cusgrsize  29541  erclwwlkref  30108  erclwwlksym  30109  erclwwlknref  30157  erclwwlknsym  30158  eclclwwlkn1  30163  gonanegoal  35553  gonarlem  35595  gonar  35596  fmla0disjsuc  35599  fmlasucdisj  35600  mclsppslem  35784  fneer  36554  curunc  37940  matunitlindflem2  37955  vvdifopab  38603  inxprnres  38636  ineccnvmo  38695  alrmomorn  38696  dfsucmap3  38801  dmsucmap  38806  dfcoss2  38841  dfcoss3  38842  cosscnv  38844  cocossss  38864  cnvcosseq  38865  refressn  38871  antisymressn  38872  trressn  38873  rncossdmcoss  38883  symrelcoss3  38893  1cosscnvxrn  38903  cosscnvssid3  38904  cosscnvssid4  38905  coss0  38907  trcoss  38910  trcoss2  38912  erimeq2  39101  dfeldisj3  39149  dfeldisj4  39150  eldisjdmqsim  39155  dfantisymrel5  39203  dfpetparts2  39310  dfpeters2  39312  ismrc  43150  en2pr  43995  pr2cv  43996  permaxext  45453  permac8prim  45462  ovnsubaddlem1  47019  sprsymrelfvlem  47965  sprsymrelf1lem  47966  prprelb  47991  prprspr2  47993  reuprpr  47998  2exopprim  48000  reuopreuprim  48001