Theorem elv 2713

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

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 1481  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-ext 2136

This theorem depends on definitions:  df-bi 116  df-sb 1740  df-clab 2141  df-cleq 2147  df-clel 2150  df-v 2711

This theorem is referenced by:  xpiindim  4716  disjxp1  6173  ixpiinm  6658  ixpsnf1o  6670  iunfidisj  6879  ssfii  6907  fifo  6913  omp1eomlem  7024  exmidomniim  7063  bcval5  10614  rexfiuz  10866  fsum2dlemstep  11308  fsumcnv  11311  fisumcom2  11312  fsumconst  11328  modfsummodlemstep  11331  fsumabs  11339  fprodcllemf  11487  fprod2dlemstep  11496  fprodcnv  11499  fprodcom2fi  11500  fprodmodd  11515  ennnfonelemim  12104  topnfn  12295  iuncld  12454  txbas  12597  txdis  12616  xmetunirn  12697  xmettxlem  12848  xmettx  12849  pw1nct  13514