Theorem elv 2825

Description: Technical lemma used to shorten proofs. If a proposition is implied by x e. _V (which is true, see vex 2824), 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 2824	. 2 |- x e. _V
2		elv.1	. 2 |- ( x e. _V -> ph )
3	1, 2	ax-mp 5	1 |- ph

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   _Vcvv 2821

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-v 2823

This theorem is used by:  xpiindim  4917  disjxp1  6472  cnvimadfsn  6485  ixpiinm  7006  ixpsnf1o  7018  modom  7108  eqsndc  7210  iunfidisj  7260  ssfii  7308  fifo  7314  dcfi  7315  omp1eomlem  7434  exmidomniim  7481  bcval5  11215  hashmap  11282  hashfibclem  11296  hashf1lem2  11300  hashf1  11301  rexfiuz  11769  fsum2dlemstep  12217  fsumcnv  12220  fisumcom2  12221  fsumconst  12237  modfsummodlemstep  12240  fsumabs  12248  fprodcllemf  12396  fprod2dlemstep  12405  fprodcnv  12408  fprodcom2fi  12409  fprodmodd  12424  4sqleminfi  13196  ennnfonelemim  13364  topnfn  13647  ptex  13667  prdsvallem  13670  xpsff1o  13719  ismgm  13726  issgrp  13767  ismnddef  13780  isnsg  14054  gsumconstcmn  14215  prdsval  14222  fnmgp  14268  isrng  14282  isring  14353  dfrhm2  14510  znval  15020  iuncld  15265  txbas  15408  txdis  15427  xmetunirn  15508  xmettxlem  15659  xmettx  15660  logfac  16048  gausslemma2dlem1a  16275  isuhgrm  16410  isushgrm  16411  isupgren  16434  upgrex  16442  isumgren  16444  isuspgren  16496  isusgren  16497  vtxdgfval  16627  clwwlknon  16768  pw1nct  17131