Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  elv GIF version

Theorem elv 2716
 Description: Technical lemma used to shorten proofs. If a proposition is implied by 𝑥 ∈ V (which is true, see vex 2715), 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
StepHypRef Expression
1 vex 2715 . 2 𝑥 ∈ V
2 elv.1 . 2 (𝑥 ∈ V → 𝜑)
31, 2ax-mp 5 1 𝜑
 Colors of variables: wff set class Syntax hints:   → wi 4   ∈ wcel 2128  Vcvv 2712 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 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-ext 2139 This theorem depends on definitions:  df-bi 116  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-v 2714 This theorem is referenced by:  xpiindim  4720  disjxp1  6177  ixpiinm  6662  ixpsnf1o  6674  iunfidisj  6883  ssfii  6911  fifo  6917  omp1eomlem  7028  exmidomniim  7067  bcval5  10619  rexfiuz  10871  fsum2dlemstep  11313  fsumcnv  11316  fisumcom2  11317  fsumconst  11333  modfsummodlemstep  11336  fsumabs  11344  fprodcllemf  11492  fprod2dlemstep  11501  fprodcnv  11504  fprodcom2fi  11505  fprodmodd  11520  ennnfonelemim  12125  topnfn  12316  iuncld  12475  txbas  12618  txdis  12637  xmetunirn  12718  xmettxlem  12869  xmettx  12870  pw1nct  13535
 Copyright terms: Public domain W3C validator