Theorem elv 2767

Description: Technical lemma used to shorten proofs. If a proposition is implied by 𝑥 ∈ V (which is true, see vex 2766), then it is true. (Contributed by Peter Mazsa, 13-Oct-2018.)

Hypothesis

Ref	Expression
elv.1	⊢ (𝑥 ∈ V → 𝜑)

Assertion

Ref	Expression
elv	⊢ 𝜑

Proof of Theorem elv

Step	Hyp	Ref	Expression
1		vex 2766	. 2 ⊢ 𝑥 ∈ V
2		elv.1	. 2 ⊢ (𝑥 ∈ V → 𝜑)
3	1, 2	ax-mp 5	1 ⊢ 𝜑

Syntax hints:   → wi 4   ∈ 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  6303  ixpiinm  6792  ixpsnf1o  6804  iunfidisj  7021  ssfii  7049  fifo  7055  dcfi  7056  omp1eomlem  7169  exmidomniim  7216  bcval5  10872  rexfiuz  11171  fsum2dlemstep  11616  fsumcnv  11619  fisumcom2  11620  fsumconst  11636  modfsummodlemstep  11639  fsumabs  11647  fprodcllemf  11795  fprod2dlemstep  11804  fprodcnv  11807  fprodcom2fi  11808  fprodmodd  11823  4sqleminfi  12591  ennnfonelemim  12666  topnfn  12946  ptex  12966  prdsvallem  12974  prdsval  12975  xpsff1o  13051  ismgm  13059  issgrp  13105  ismnddef  13120  isnsg  13408  fnmgp  13554  isrng  13566  isring  13632  dfrhm2  13786  znval  14268  iuncld  14435  txbas  14578  txdis  14597  xmetunirn  14678  xmettxlem  14829  xmettx  14830  gausslemma2dlem1a  15383  pw1nct  15734