Theorem elv 2756

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

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-v 2754

This theorem is referenced by:  xpiindim  4782  disjxp1  6261  ixpiinm  6750  ixpsnf1o  6762  iunfidisj  6975  ssfii  7003  fifo  7009  dcfi  7010  omp1eomlem  7123  exmidomniim  7169  bcval5  10775  rexfiuz  11030  fsum2dlemstep  11474  fsumcnv  11477  fisumcom2  11478  fsumconst  11494  modfsummodlemstep  11497  fsumabs  11505  fprodcllemf  11653  fprod2dlemstep  11662  fprodcnv  11665  fprodcom2fi  11666  fprodmodd  11681  4sqleminfi  12429  ennnfonelemim  12475  topnfn  12749  ptex  12769  xpsff1o  12825  ismgm  12833  issgrp  12866  ismnddef  12879  isnsg  13141  fnmgp  13276  isrng  13288  isring  13354  dfrhm2  13504  znval  13932  iuncld  14075  txbas  14218  txdis  14237  xmetunirn  14318  xmettxlem  14469  xmettx  14470  pw1nct  15214