Theorem elv 2767

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

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-v 2765

This theorem is referenced by:  xpiindim  4803  disjxp1  6294  ixpiinm  6783  ixpsnf1o  6795  iunfidisj  7012  ssfii  7040  fifo  7046  dcfi  7047  omp1eomlem  7160  exmidomniim  7207  bcval5  10855  rexfiuz  11154  fsum2dlemstep  11599  fsumcnv  11602  fisumcom2  11603  fsumconst  11619  modfsummodlemstep  11622  fsumabs  11630  fprodcllemf  11778  fprod2dlemstep  11787  fprodcnv  11790  fprodcom2fi  11791  fprodmodd  11806  4sqleminfi  12566  ennnfonelemim  12641  topnfn  12915  ptex  12935  xpsff1o  12992  ismgm  13000  issgrp  13046  ismnddef  13059  isnsg  13332  fnmgp  13478  isrng  13490  isring  13556  dfrhm2  13710  znval  14192  iuncld  14351  txbas  14494  txdis  14513  xmetunirn  14594  xmettxlem  14745  xmettx  14746  gausslemma2dlem1a  15299  pw1nct  15647