Theorem el2v 3487

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482

This theorem is referenced by:  codir  6140  dfco2  6265  1st2val  8042  2nd2val  8043  fnmap  8873  enrefnn  9087  unfi  9211  wemappo  9589  wemapsolem  9590  fin23lem26  10365  seqval  14053  hash2exprb  14510  hashle2prv  14517  hash3tpexb  14533  mreexexlem4d  17690  pmtrrn2  19478  c0snmgmhm  20462  alexsubALTlem4  24058  elqaalem2  26362  seqsval  28294  upgrex  29109  cusgrsize  29472  erclwwlkref  30039  erclwwlksym  30040  erclwwlknref  30088  erclwwlknsym  30089  eclclwwlkn1  30094  gonanegoal  35357  gonarlem  35399  gonar  35400  fmla0disjsuc  35403  fmlasucdisj  35404  mclsppslem  35588  fneer  36354  curunc  37609  matunitlindflem2  37624  vvdifopab  38261  inxprnres  38293  ineccnvmo  38358  alrmomorn  38359  dfcoss2  38414  dfcoss3  38415  cosscnv  38417  cocossss  38437  cnvcosseq  38438  refressn  38444  antisymressn  38445  trressn  38446  rncossdmcoss  38456  symrelcoss3  38466  1cosscnvxrn  38476  cosscnvssid3  38477  cosscnvssid4  38478  coss0  38480  trcoss  38483  trcoss2  38485  erimeq2  38679  dfeldisj3  38720  dfeldisj4  38721  dfantisymrel5  38763  ismrc  42712  en2pr  43560  pr2cv  43561  ovnsubaddlem1  46585  sprsymrelfvlem  47477  sprsymrelf1lem  47478  prprelb  47503  prprspr2  47505  reuprpr  47510  2exopprim  47512  reuopreuprim  47513