Theorem elv 2807

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

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 2213

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

This theorem is referenced by:  xpiindim  4873  disjxp1  6410  cnvimadfsn  6423  ixpiinm  6936  ixpsnf1o  6948  modom  7037  eqsndc  7138  iunfidisj  7188  ssfii  7233  fifo  7239  dcfi  7240  omp1eomlem  7353  exmidomniim  7400  bcval5  11088  rexfiuz  11629  fsum2dlemstep  12075  fsumcnv  12078  fisumcom2  12079  fsumconst  12095  modfsummodlemstep  12098  fsumabs  12106  fprodcllemf  12254  fprod2dlemstep  12263  fprodcnv  12266  fprodcom2fi  12267  fprodmodd  12282  4sqleminfi  13050  ennnfonelemim  13125  topnfn  13407  ptex  13427  prdsvallem  13435  prdsval  13436  xpsff1o  13512  ismgm  13520  issgrp  13566  ismnddef  13581  isnsg  13869  fnmgp  14016  isrng  14028  isring  14094  dfrhm2  14249  znval  14732  iuncld  14926  txbas  15069  txdis  15088  xmetunirn  15169  xmettxlem  15320  xmettx  15321  gausslemma2dlem1a  15877  isuhgrm  16012  isushgrm  16013  isupgren  16036  upgrex  16044  isumgren  16046  isuspgren  16098  isusgren  16099  vtxdgfval  16229  clwwlknon  16370  pw1nct  16725