Theorem elv 2803

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

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-v 2801

This theorem is referenced by:  xpiindim  4859  disjxp1  6382  ixpiinm  6871  ixpsnf1o  6883  iunfidisj  7113  ssfii  7141  fifo  7147  dcfi  7148  omp1eomlem  7261  exmidomniim  7308  bcval5  10985  rexfiuz  11500  fsum2dlemstep  11945  fsumcnv  11948  fisumcom2  11949  fsumconst  11965  modfsummodlemstep  11968  fsumabs  11976  fprodcllemf  12124  fprod2dlemstep  12133  fprodcnv  12136  fprodcom2fi  12137  fprodmodd  12152  4sqleminfi  12920  ennnfonelemim  12995  topnfn  13277  ptex  13297  prdsvallem  13305  prdsval  13306  xpsff1o  13382  ismgm  13390  issgrp  13436  ismnddef  13451  isnsg  13739  fnmgp  13885  isrng  13897  isring  13963  dfrhm2  14118  znval  14600  iuncld  14789  txbas  14932  txdis  14951  xmetunirn  15032  xmettxlem  15183  xmettx  15184  gausslemma2dlem1a  15737  isuhgrm  15871  isushgrm  15872  isupgren  15895  upgrex  15903  isumgren  15905  isuspgren  15955  isusgren  15956  pw1nct  16369