Theorem el2v 3457

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2144  Vcvv 3450

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452

This theorem is used by:  codir  6116  dfco2  6249  1st2val  8033  2nd2val  8034  fnmap  8861  enrefnn  9082  unfi  9194  wemappo  9550  wemapsolem  9551  fin23lem26  10410  seqval  14162  hash2exprb  14623  hashle2prv  14630  hash3tpexb  14646  mreexexlem4d  17830  pmtrrn2  19683  c0snmgmhm  20701  matunitlindflem2  23004  alexsubALTlem4  24378  elqaalem2  26652  seqsval  28683  upgrex  29679  cusgrsize  30044  erclwwlkref  30620  erclwwlksym  30621  erclwwlknref  30669  erclwwlknsym  30670  eclclwwlkn1  30675  onvfowev  36001  gonanegoal  36235  gonarlem  36277  gonar  36278  fmla0disjsuc  36281  fmlasucdisj  36282  mclsppslem  36466  fneer  37265  curunc  38662  findcard4  38769  vvdifopab  39334  inxprnres  39367  ineccnvmo  39426  alrmomorn  39427  dfsucmap3  39532  dmsucmap  39537  dfcoss2  39572  dfcoss3  39573  cosscnv  39575  cocossss  39595  cnvcosseq  39596  refressn  39602  antisymressn  39603  trressn  39604  rncossdmcoss  39614  symrelcoss3  39624  1cosscnvxrn  39634  cosscnvssid3  39635  cosscnvssid4  39636  coss0  39638  trcoss  39641  trcoss2  39643  erimeq2  39832  dfeldisj3  39880  dfeldisj4  39881  eldisjdmqsim  39886  dfantisymrel5  39934  dfpetparts2  40041  dfpeters2  40043  ismrc  43849  en2pr  44685  pr2cv  44686  permaxext  46131  permac8prim  46140  ovnsubaddlem1  47716  sprsymrelfvlem  48708  sprsymrelf1lem  48709  prprelb  48734  prprspr2  48736  reuprpr  48741  2exopprim  48743  reuopreuprim  48744