Theorem elv 2767

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

Syntax hints:   → wi 4   ∈ wcel 2167  Vcvv 2763

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-v 2765

This theorem is referenced by:  xpiindim  4804  disjxp1  6303  ixpiinm  6792  ixpsnf1o  6804  iunfidisj  7021  ssfii  7049  fifo  7055  dcfi  7056  omp1eomlem  7169  exmidomniim  7216  bcval5  10874  rexfiuz  11173  fsum2dlemstep  11618  fsumcnv  11621  fisumcom2  11622  fsumconst  11638  modfsummodlemstep  11641  fsumabs  11649  fprodcllemf  11797  fprod2dlemstep  11806  fprodcnv  11809  fprodcom2fi  11810  fprodmodd  11825  4sqleminfi  12593  ennnfonelemim  12668  topnfn  12948  ptex  12968  prdsvallem  12976  prdsval  12977  xpsff1o  13053  ismgm  13061  issgrp  13107  ismnddef  13122  isnsg  13410  fnmgp  13556  isrng  13568  isring  13634  dfrhm2  13788  znval  14270  iuncld  14459  txbas  14602  txdis  14621  xmetunirn  14702  xmettxlem  14853  xmettx  14854  gausslemma2dlem1a  15407  pw1nct  15758