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  6401  ixpiinm  6893  ixpsnf1o  6905  modom  6994  eqsndc  7095  iunfidisj  7145  ssfii  7173  fifo  7179  dcfi  7180  omp1eomlem  7293  exmidomniim  7340  bcval5  11026  rexfiuz  11554  fsum2dlemstep  12000  fsumcnv  12003  fisumcom2  12004  fsumconst  12020  modfsummodlemstep  12023  fsumabs  12031  fprodcllemf  12179  fprod2dlemstep  12188  fprodcnv  12191  fprodcom2fi  12192  fprodmodd  12207  4sqleminfi  12975  ennnfonelemim  13050  topnfn  13332  ptex  13352  prdsvallem  13360  prdsval  13361  xpsff1o  13437  ismgm  13445  issgrp  13491  ismnddef  13506  isnsg  13794  fnmgp  13941  isrng  13953  isring  14019  dfrhm2  14174  znval  14656  iuncld  14845  txbas  14988  txdis  15007  xmetunirn  15088  xmettxlem  15239  xmettx  15240  gausslemma2dlem1a  15793  isuhgrm  15928  isushgrm  15929  isupgren  15952  upgrex  15960  isumgren  15962  isuspgren  16014  isusgren  16015  vtxdgfval  16145  clwwlknon  16286  pw1nct  16630