Theorem elv 2806

Description: Technical lemma used to shorten proofs. If a proposition is implied by x e. _V (which is true, see vex 2805), 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 2805	. 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 2202   _Vcvv 2802

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-v 2804

This theorem is referenced by:  xpiindim  4867  disjxp1  6401  ixpiinm  6893  ixpsnf1o  6905  modom  6994  eqsndc  7095  iunfidisj  7145  ssfii  7173  fifo  7179  dcfi  7180  omp1eomlem  7293  exmidomniim  7340  bcval5  11026  rexfiuz  11567  fsum2dlemstep  12013  fsumcnv  12016  fisumcom2  12017  fsumconst  12033  modfsummodlemstep  12036  fsumabs  12044  fprodcllemf  12192  fprod2dlemstep  12201  fprodcnv  12204  fprodcom2fi  12205  fprodmodd  12220  4sqleminfi  12988  ennnfonelemim  13063  topnfn  13345  ptex  13365  prdsvallem  13373  prdsval  13374  xpsff1o  13450  ismgm  13458  issgrp  13504  ismnddef  13519  isnsg  13807  fnmgp  13954  isrng  13966  isring  14032  dfrhm2  14187  znval  14669  iuncld  14858  txbas  15001  txdis  15020  xmetunirn  15101  xmettxlem  15252  xmettx  15253  gausslemma2dlem1a  15806  isuhgrm  15941  isushgrm  15942  isupgren  15965  upgrex  15973  isumgren  15975  isuspgren  16027  isusgren  16028  vtxdgfval  16158  clwwlknon  16299  pw1nct  16655