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  4799  disjxp1  6289  ixpiinm  6778  ixpsnf1o  6790  iunfidisj  7005  ssfii  7033  fifo  7039  dcfi  7040  omp1eomlem  7153  exmidomniim  7200  bcval5  10834  rexfiuz  11133  fsum2dlemstep  11577  fsumcnv  11580  fisumcom2  11581  fsumconst  11597  modfsummodlemstep  11600  fsumabs  11608  fprodcllemf  11756  fprod2dlemstep  11765  fprodcnv  11768  fprodcom2fi  11769  fprodmodd  11784  4sqleminfi  12535  ennnfonelemim  12581  topnfn  12855  ptex  12875  xpsff1o  12932  ismgm  12940  issgrp  12986  ismnddef  12999  isnsg  13272  fnmgp  13418  isrng  13430  isring  13496  dfrhm2  13650  znval  14124  iuncld  14283  txbas  14426  txdis  14445  xmetunirn  14526  xmettxlem  14677  xmettx  14678  gausslemma2dlem1a  15174  pw1nct  15493