Theorem elv 2806

Description: Technical lemma used to shorten proofs. If a proposition is implied by 𝑥 ∈ V (which is true, see vex 2805), 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 2805	. 2 ⊢ 𝑥 ∈ V
2		elv.1	. 2 ⊢ (𝑥 ∈ V → 𝜑)
3	1, 2	ax-mp 5	1 ⊢ 𝜑

Syntax hints:   → wi 4   ∈ wcel 2202  Vcvv 2802

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-v 2804

This theorem is referenced by:  xpiindim  4867  disjxp1  6400  ixpiinm  6892  ixpsnf1o  6904  modom  6993  eqsndc  7094  iunfidisj  7144  ssfii  7172  fifo  7178  dcfi  7179  omp1eomlem  7292  exmidomniim  7339  bcval5  11024  rexfiuz  11549  fsum2dlemstep  11994  fsumcnv  11997  fisumcom2  11998  fsumconst  12014  modfsummodlemstep  12017  fsumabs  12025  fprodcllemf  12173  fprod2dlemstep  12182  fprodcnv  12185  fprodcom2fi  12186  fprodmodd  12201  4sqleminfi  12969  ennnfonelemim  13044  topnfn  13326  ptex  13346  prdsvallem  13354  prdsval  13355  xpsff1o  13431  ismgm  13439  issgrp  13485  ismnddef  13500  isnsg  13788  fnmgp  13934  isrng  13946  isring  14012  dfrhm2  14167  znval  14649  iuncld  14838  txbas  14981  txdis  15000  xmetunirn  15081  xmettxlem  15232  xmettx  15233  gausslemma2dlem1a  15786  isuhgrm  15921  isushgrm  15922  isupgren  15945  upgrex  15953  isumgren  15955  isuspgren  16007  isusgren  16008  vtxdgfval  16138  clwwlknon  16279  pw1nct  16604