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

Theorem elv 2713
 Description: Technical lemma used to shorten proofs. If a proposition is implied by (which is true, see vex 2712), then it is true. (Contributed by Peter Mazsa, 13-Oct-2018.)
Hypothesis
Ref Expression
elv.1
Assertion
Ref Expression
elv

Proof of Theorem elv
StepHypRef Expression
1 vex 2712 . 2
2 elv.1 . 2
31, 2ax-mp 5 1
 Colors of variables: wff set class Syntax hints:   wi 4   wcel 2125  cvv 2709 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 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1481  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-ext 2136 This theorem depends on definitions:  df-bi 116  df-sb 1740  df-clab 2141  df-cleq 2147  df-clel 2150  df-v 2711 This theorem is referenced by:  xpiindim  4716  disjxp1  6173  ixpiinm  6658  ixpsnf1o  6670  iunfidisj  6879  ssfii  6907  fifo  6913  omp1eomlem  7024  exmidomniim  7063  bcval5  10614  rexfiuz  10866  fsum2dlemstep  11308  fsumcnv  11311  fisumcom2  11312  fsumconst  11328  modfsummodlemstep  11331  fsumabs  11339  fprodcllemf  11487  fprod2dlemstep  11496  fprodcnv  11499  fprodcom2fi  11500  fprodmodd  11515  ennnfonelemim  12104  topnfn  12295  iuncld  12454  txbas  12597  txdis  12616  xmetunirn  12697  xmettxlem  12848  xmettx  12849  pw1nct  13514
 Copyright terms: Public domain W3C validator