Theorem el2v 3449

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

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

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 3444

This theorem is referenced by:  codir  6085  dfco2  6211  1st2val  7971  2nd2val  7972  fnmap  8782  enrefnn  8995  unfi  9107  wemappo  9466  wemapsolem  9467  fin23lem26  10247  seqval  13947  hash2exprb  14406  hashle2prv  14413  hash3tpexb  14429  mreexexlem4d  17582  pmtrrn2  19401  c0snmgmhm  20410  alexsubALTlem4  24006  elqaalem2  26296  seqsval  28296  upgrex  29177  cusgrsize  29540  erclwwlkref  30107  erclwwlksym  30108  erclwwlknref  30156  erclwwlknsym  30157  eclclwwlkn1  30162  gonanegoal  35568  gonarlem  35610  gonar  35611  fmla0disjsuc  35614  fmlasucdisj  35615  mclsppslem  35799  fneer  36569  curunc  37853  matunitlindflem2  37868  vvdifopab  38516  inxprnres  38549  ineccnvmo  38608  alrmomorn  38609  dfsucmap3  38714  dmsucmap  38719  dfcoss2  38754  dfcoss3  38755  cosscnv  38757  cocossss  38777  cnvcosseq  38778  refressn  38784  antisymressn  38785  trressn  38786  rncossdmcoss  38796  symrelcoss3  38806  1cosscnvxrn  38816  cosscnvssid3  38817  cosscnvssid4  38818  coss0  38820  trcoss  38823  trcoss2  38825  erimeq2  39014  dfeldisj3  39062  dfeldisj4  39063  eldisjdmqsim  39068  dfantisymrel5  39116  dfpetparts2  39223  dfpeters2  39225  ismrc  43058  en2pr  43903  pr2cv  43904  permaxext  45361  permac8prim  45370  ovnsubaddlem1  46928  sprsymrelfvlem  47850  sprsymrelf1lem  47851  prprelb  47876  prprspr2  47878  reuprpr  47883  2exopprim  47885  reuopreuprim  47886