Theorem elv 2743

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

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-v 2741

This theorem is referenced by:  xpiindim  4766  disjxp1  6239  ixpiinm  6726  ixpsnf1o  6738  iunfidisj  6947  ssfii  6975  fifo  6981  dcfi  6982  omp1eomlem  7095  exmidomniim  7141  bcval5  10745  rexfiuz  11000  fsum2dlemstep  11444  fsumcnv  11447  fisumcom2  11448  fsumconst  11464  modfsummodlemstep  11467  fsumabs  11475  fprodcllemf  11623  fprod2dlemstep  11632  fprodcnv  11635  fprodcom2fi  11636  fprodmodd  11651  ennnfonelemim  12427  topnfn  12698  ptex  12718  xpsff1o  12773  ismgm  12781  issgrp  12814  ismnddef  12824  isnsg  13067  fnmgp  13137  isring  13188  iuncld  13654  txbas  13797  txdis  13816  xmetunirn  13897  xmettxlem  14048  xmettx  14049  pw1nct  14791