Theorem elv 2776

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

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-v 2774

This theorem is referenced by:  xpiindim  4816  disjxp1  6324  ixpiinm  6813  ixpsnf1o  6825  iunfidisj  7050  ssfii  7078  fifo  7084  dcfi  7085  omp1eomlem  7198  exmidomniim  7245  bcval5  10910  rexfiuz  11333  fsum2dlemstep  11778  fsumcnv  11781  fisumcom2  11782  fsumconst  11798  modfsummodlemstep  11801  fsumabs  11809  fprodcllemf  11957  fprod2dlemstep  11966  fprodcnv  11969  fprodcom2fi  11970  fprodmodd  11985  4sqleminfi  12753  ennnfonelemim  12828  topnfn  13109  ptex  13129  prdsvallem  13137  prdsval  13138  xpsff1o  13214  ismgm  13222  issgrp  13268  ismnddef  13283  isnsg  13571  fnmgp  13717  isrng  13729  isring  13795  dfrhm2  13949  znval  14431  iuncld  14620  txbas  14763  txdis  14782  xmetunirn  14863  xmettxlem  15014  xmettx  15015  gausslemma2dlem1a  15568  pw1nct  15977