Theorem elv 2816

Description: Technical lemma used to shorten proofs. If a proposition is implied by x e. _V (which is true, see vex 2815), then it is true. (Contributed by Peter Mazsa, 13-Oct-2018.)

Hypothesis

Ref	Expression
elv.1	|- ( x e. _V -> ph )

Assertion

Ref	Expression
elv	|- ph

Proof of Theorem elv

Step	Hyp	Ref	Expression
1		vex 2815	. 2 |- x e. _V
2		elv.1	. 2 |- ( x e. _V -> ph )
3	1, 2	ax-mp 5	1 |- ph

Syntax hints:   -> wi 4   e. wcel 2203   _Vcvv 2812

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-v 2814

This theorem is referenced by:  xpiindim  4891  disjxp1  6431  cnvimadfsn  6444  ixpiinm  6958  ixpsnf1o  6970  modom  7060  eqsndc  7162  iunfidisj  7212  ssfii  7260  fifo  7266  dcfi  7267  omp1eomlem  7384  exmidomniim  7431  bcval5  11124  hashfibclem  11202  rexfiuz  11670  fsum2dlemstep  12116  fsumcnv  12119  fisumcom2  12120  fsumconst  12136  modfsummodlemstep  12139  fsumabs  12147  fprodcllemf  12295  fprod2dlemstep  12304  fprodcnv  12307  fprodcom2fi  12308  fprodmodd  12323  4sqleminfi  13091  ennnfonelemim  13167  topnfn  13449  ptex  13469  prdsvallem  13477  prdsval  13478  xpsff1o  13554  ismgm  13562  issgrp  13608  ismnddef  13623  isnsg  13911  fnmgp  14058  isrng  14070  isring  14136  dfrhm2  14291  znval  14776  iuncld  14972  txbas  15115  txdis  15134  xmetunirn  15215  xmettxlem  15366  xmettx  15367  gausslemma2dlem1a  15923  isuhgrm  16058  isushgrm  16059  isupgren  16082  upgrex  16090  isumgren  16092  isuspgren  16144  isusgren  16145  vtxdgfval  16275  clwwlknon  16416  pw1nct  16769