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

Theorem elv 2741
Description: Technical lemma used to shorten proofs. If a proposition is implied by  x  e.  _V (which is true, see vex 2740), then it is true. (Contributed by Peter Mazsa, 13-Oct-2018.)
Hypothesis
Ref Expression
elv.1  |-  ( x  e.  _V  ->  ph )
Assertion
Ref Expression
elv  |-  ph

Proof of Theorem elv
StepHypRef Expression
1 vex 2740 . 2  |-  x  e. 
_V
2 elv.1 . 2  |-  ( x  e.  _V  ->  ph )
31, 2ax-mp 5 1  |-  ph
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 2148   _Vcvv 2737
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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-v 2739
This theorem is referenced by:  xpiindim  4759  disjxp1  6230  ixpiinm  6717  ixpsnf1o  6729  iunfidisj  6938  ssfii  6966  fifo  6972  dcfi  6973  omp1eomlem  7086  exmidomniim  7132  bcval5  10714  rexfiuz  10969  fsum2dlemstep  11413  fsumcnv  11416  fisumcom2  11417  fsumconst  11433  modfsummodlemstep  11436  fsumabs  11444  fprodcllemf  11592  fprod2dlemstep  11601  fprodcnv  11604  fprodcom2fi  11605  fprodmodd  11620  ennnfonelemim  12395  topnfn  12628  ismgm  12655  issgrp  12688  ismnddef  12698  fnmgp  12946  isring  12996  iuncld  13248  txbas  13391  txdis  13410  xmetunirn  13491  xmettxlem  13642  xmettx  13643  pw1nct  14375
  Copyright terms: Public domain W3C validator