Theorem elv 2776

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

Syntax hints:   → wi 4   ∈ wcel 2176  Vcvv 2772

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-v 2774

This theorem is referenced by:  xpiindim  4815  disjxp1  6322  ixpiinm  6811  ixpsnf1o  6823  iunfidisj  7048  ssfii  7076  fifo  7082  dcfi  7083  omp1eomlem  7196  exmidomniim  7243  bcval5  10908  rexfiuz  11300  fsum2dlemstep  11745  fsumcnv  11748  fisumcom2  11749  fsumconst  11765  modfsummodlemstep  11768  fsumabs  11776  fprodcllemf  11924  fprod2dlemstep  11933  fprodcnv  11936  fprodcom2fi  11937  fprodmodd  11952  4sqleminfi  12720  ennnfonelemim  12795  topnfn  13076  ptex  13096  prdsvallem  13104  prdsval  13105  xpsff1o  13181  ismgm  13189  issgrp  13235  ismnddef  13250  isnsg  13538  fnmgp  13684  isrng  13696  isring  13762  dfrhm2  13916  znval  14398  iuncld  14587  txbas  14730  txdis  14749  xmetunirn  14830  xmettxlem  14981  xmettx  14982  gausslemma2dlem1a  15535  pw1nct  15940