Theorem elv 2730

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

Syntax hints:   → wi 4   ∈ wcel 2136  Vcvv 2726

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-v 2728

This theorem is referenced by:  xpiindim  4741  disjxp1  6204  ixpiinm  6690  ixpsnf1o  6702  iunfidisj  6911  ssfii  6939  fifo  6945  dcfi  6946  omp1eomlem  7059  exmidomniim  7105  bcval5  10676  rexfiuz  10931  fsum2dlemstep  11375  fsumcnv  11378  fisumcom2  11379  fsumconst  11395  modfsummodlemstep  11398  fsumabs  11406  fprodcllemf  11554  fprod2dlemstep  11563  fprodcnv  11566  fprodcom2fi  11567  fprodmodd  11582  ennnfonelemim  12357  topnfn  12561  ismgm  12588  iuncld  12755  txbas  12898  txdis  12917  xmetunirn  12998  xmettxlem  13149  xmettx  13150  pw1nct  13883