Theorem elv 2764

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

Syntax hints:   → wi 4   ∈ wcel 2164  Vcvv 2760

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-v 2762

This theorem is referenced by:  xpiindim  4800  disjxp1  6291  ixpiinm  6780  ixpsnf1o  6792  iunfidisj  7007  ssfii  7035  fifo  7041  dcfi  7042  omp1eomlem  7155  exmidomniim  7202  bcval5  10837  rexfiuz  11136  fsum2dlemstep  11580  fsumcnv  11583  fisumcom2  11584  fsumconst  11600  modfsummodlemstep  11603  fsumabs  11611  fprodcllemf  11759  fprod2dlemstep  11768  fprodcnv  11771  fprodcom2fi  11772  fprodmodd  11787  4sqleminfi  12538  ennnfonelemim  12584  topnfn  12858  ptex  12878  xpsff1o  12935  ismgm  12943  issgrp  12989  ismnddef  13002  isnsg  13275  fnmgp  13421  isrng  13433  isring  13499  dfrhm2  13653  znval  14135  iuncld  14294  txbas  14437  txdis  14456  xmetunirn  14537  xmettxlem  14688  xmettx  14689  gausslemma2dlem1a  15215  pw1nct  15563