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  4804  disjxp1  6296  ixpiinm  6785  ixpsnf1o  6797  iunfidisj  7014  ssfii  7042  fifo  7048  dcfi  7049  omp1eomlem  7162  exmidomniim  7209  bcval5  10858  rexfiuz  11157  fsum2dlemstep  11602  fsumcnv  11605  fisumcom2  11606  fsumconst  11622  modfsummodlemstep  11625  fsumabs  11633  fprodcllemf  11781  fprod2dlemstep  11790  fprodcnv  11793  fprodcom2fi  11794  fprodmodd  11809  4sqleminfi  12577  ennnfonelemim  12652  topnfn  12932  ptex  12952  prdsvallem  12960  prdsval  12961  xpsff1o  13018  ismgm  13026  issgrp  13072  ismnddef  13085  isnsg  13358  fnmgp  13504  isrng  13516  isring  13582  dfrhm2  13736  znval  14218  iuncld  14377  txbas  14520  txdis  14539  xmetunirn  14620  xmettxlem  14771  xmettx  14772  gausslemma2dlem1a  15325  pw1nct  15674