Theorem el2v 3495

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  Vcvv 3488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490

This theorem is referenced by:  codir  6152  dfco2  6276  1st2val  8058  2nd2val  8059  fnmap  8891  enrefnn  9113  unfi  9238  wemappo  9618  wemapsolem  9619  fin23lem26  10394  seqval  14063  hash2exprb  14520  hashle2prv  14527  hash3tpexb  14543  mreexexlem4d  17705  pmtrrn2  19502  c0snmgmhm  20488  alexsubALTlem4  24079  elqaalem2  26380  seqsval  28312  upgrex  29127  cusgrsize  29490  erclwwlkref  30052  erclwwlksym  30053  erclwwlknref  30101  erclwwlknsym  30102  eclclwwlkn1  30107  gonanegoal  35320  gonarlem  35362  gonar  35363  fmla0disjsuc  35366  fmlasucdisj  35367  mclsppslem  35551  fneer  36319  curunc  37562  matunitlindflem2  37577  vvdifopab  38216  inxprnres  38248  ineccnvmo  38313  alrmomorn  38314  dfcoss2  38369  dfcoss3  38370  cosscnv  38372  cocossss  38392  cnvcosseq  38393  refressn  38399  antisymressn  38400  trressn  38401  rncossdmcoss  38411  symrelcoss3  38421  1cosscnvxrn  38431  cosscnvssid3  38432  cosscnvssid4  38433  coss0  38435  trcoss  38438  trcoss2  38440  erimeq2  38634  dfeldisj3  38675  dfeldisj4  38676  dfantisymrel5  38718  ismrc  42657  en2pr  43509  pr2cv  43510  ovnsubaddlem1  46491  sprsymrelfvlem  47364  sprsymrelf1lem  47365  prprelb  47390  prprspr2  47392  reuprpr  47397  2exopprim  47399  reuopreuprim  47400