MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  exp4a Unicode version

Theorem exp4a 606
Description: An exportation inference. (Contributed by NM, 26-Apr-1994.)
Hypothesis
Ref Expression
exp4a.1
Assertion
Ref Expression
exp4a

Proof of Theorem exp4a
StepHypRef Expression
1 exp4a.1 . 2
2 impexp 446 . 2
31, 2syl6ib 226 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  exp4b  607  exp4d  609  exp45  614  exp5c  616  tz7.7  4909  tfr3  7087  oaass  7229  omordi  7234  nnmordi  7299  fiint  7817  zorn2lem6  8902  zorn2lem7  8903  mulgt0sr  9503  sqlecan  12274  rexuzre  13185  caurcvg  13499  ndvdssub  14065  lsmcv  17787  iscnp4  19764  nrmsep3  19856  2ndcdisj  19957  2ndcsep  19960  tsmsxp  20657  metcnp3  21043  xrlimcnp  23298  ax5seglem5  24236  elspansn4  26491  hoadddir  26723  atcvatlem  27304  sumdmdii  27334  sumdmdlem  27337  wfrlem12  29354  frrlem11  29399  prtlem17  30617  lindslinindsimp1  33058  onfrALTlem2  33318  in3an  33397  cvratlem  35145  athgt  35180  lplnnle2at  35265  lplncvrlvol2  35339  cdlemb  35518  dalaw  35610  cdleme50trn2  36277  cdlemg18b  36405  dihmeetlem3N  37032
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
  Copyright terms: Public domain W3C validator