Theorem elv 2693

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-v 2691

This theorem is referenced by:  xpiindim  4684  disjxp1  6141  ixpiinm  6626  ixpsnf1o  6638  iunfidisj  6842  ssfii  6870  fifo  6876  omp1eomlem  6987  exmidomniim  7021  bcval5  10541  rexfiuz  10793  fsum2dlemstep  11235  fsumcnv  11238  fisumcom2  11239  fsumconst  11255  modfsummodlemstep  11258  fsumabs  11266  ennnfonelemim  11973  topnfn  12164  iuncld  12323  txbas  12466  txdis  12485  xmetunirn  12566  xmettxlem  12717  xmettx  12718  pw1nct  13371