Theorem el2v 3470

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2149  Vcvv 3463

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465

This theorem is referenced by:  codir  6121  dfco2  6247  1st2val  8014  2nd2val  8015  fnmap  8830  enrefnn  9043  unfi  9155  wemappo  9511  wemapsolem  9512  fin23lem26  10309  seqval  14048  hash2exprb  14508  hashle2prv  14515  hash3tpexb  14531  mreexexlem4d  17703  pmtrrn2  19530  c0snmgmhm  20544  alexsubALTlem4  24176  elqaalem2  26450  seqsval  28447  upgrex  29383  cusgrsize  29745  erclwwlkref  30312  erclwwlksym  30313  erclwwlknref  30361  erclwwlknsym  30362  eclclwwlkn1  30367  onvfowev  35499  gonanegoal  35743  gonarlem  35785  gonar  35786  fmla0disjsuc  35789  fmlasucdisj  35790  mclsppslem  35974  fneer  36753  curunc  38141  matunitlindflem2  38156  vvdifopab  38804  inxprnres  38837  ineccnvmo  38896  alrmomorn  38897  dfsucmap3  39002  dmsucmap  39007  dfcoss2  39042  dfcoss3  39043  cosscnv  39045  cocossss  39065  cnvcosseq  39066  refressn  39072  antisymressn  39073  trressn  39074  rncossdmcoss  39084  symrelcoss3  39094  1cosscnvxrn  39104  cosscnvssid3  39105  cosscnvssid4  39106  coss0  39108  trcoss  39111  trcoss2  39113  erimeq2  39302  dfeldisj3  39350  dfeldisj4  39351  eldisjdmqsim  39356  dfantisymrel5  39404  dfpetparts2  39511  dfpeters2  39513  ismrc  43324  en2pr  44165  pr2cv  44166  permaxext  45606  permac8prim  45615  ovnsubaddlem1  47176  sprsymrelfvlem  48128  sprsymrelf1lem  48129  prprelb  48154  prprspr2  48156  reuprpr  48161  2exopprim  48163  reuopreuprim  48164