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

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

Proof of Theorem exp43
StepHypRef Expression
1 exp43.1 . . 3
21ex 434 . 2
32exp4b 607 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  exp53  617  funssres  5633  fvopab3ig  5953  fvmptt  5971  fvn0elsuppb  6936  tfr3  7087  omordi  7234  odi  7247  nnmordi  7299  php  7721  fiint  7817  ordiso2  7961  cfcoflem  8673  zorn2lem5  8901  inar1  9174  psslinpr  9430  recexsrlem  9501  qaddcl  11227  qmulcl  11229  elfznelfzo  11915  expcan  12218  ltexp2  12219  bernneq  12292  expnbnd  12295  xpnnenOLD  13943  elcls3  19584  opnneissb  19615  txbas  20068  grpoidinvlem3  25208  grporcan  25223  shscli  26235  spansncol  26486  spanunsni  26497  spansncvi  26570  homco1  26720  homulass  26721  atomli  27301  chirredlem1  27309  cdj1i  27352  frinfm  30226  filbcmb  30231  unichnidl  30428  dmncan1  30473  initoeu2lem1  32620  scmsuppss  32965  pclfinclN  35674
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