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

Theorem exp31 587
Description: An exportation inference. (Contributed by NM, 26-Apr-1994.)
Hypothesis
Ref Expression
exp31.1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Assertion
Ref Expression
exp31  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )

Proof of Theorem exp31
StepHypRef Expression
1 exp31.1 . . 3  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
21ex 423 . 2  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
32ex 423 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  exp41  593  exp42  594  expl  601  exbiri  605  anasss  628  an31s  781  3impa  1146  exp516  1171  ax11indalem  2136  ax11inda2ALT  2137  pwssun  4299  onmindif  4482  ordsucss  4609  tfindsg  4651  mpteqb  5614  dffo3  5675  fconstfv  5734  fliftfun  5811  tfrlem9  6401  oaordi  6544  oaordex  6556  oaass  6559  oarec  6560  omlimcl  6576  omass  6578  oen0  6584  oeordsuc  6592  nnaordi  6616  omsmolem  6651  infensuc  7039  php3  7047  fisucdomOLD  7066  marypha1lem  7186  hartogs  7259  card2on  7268  tz9.12lem3  7461  infxpenlem  7641  cfflb  7885  cfcoflem  7898  cfcof  7900  isf32lem12  7990  zorn2lem6  8128  ondomon  8185  alephval2  8194  pwcfsdom  8205  axrepnd  8216  fpwwe2lem12  8263  genpcd  8630  ltexprlem6  8665  recexsr  8729  axpre-sup  8791  recex  9400  infmrcl  9733  zdiv  10082  uzaddcl  10275  rpnnen1lem5  10346  xrsupsslem  10625  xrinfmsslem  10626  supxrunb1  10638  supxrunb2  10639  seqf1o  11087  expcllem  11114  expeq0  11132  mulexp  11141  cjexp  11635  resqrex  11736  absexp  11789  summo  12190  fsum2d  12234  binom  12288  efexp  12381  demoivreALT  12481  ramcl  13076  ressress  13205  topbas  16710  fctop  16741  cctop  16743  elcls  16810  elcls3  16820  2ndcdisj  17182  filufint  17615  ovoliunlem3  18863  dvge0  19353  ulmcn  19776  grpoidinvlem4  20874  grpoinvf  20907  nmosetre  21342  ipasslem1  21409  shmodsi  21968  elspansn5  22153  normcan  22155  h1datomi  22160  nmopsetretALT  22443  nmfnsetre  22457  cnvbraval  22690  opsqrlem1  22720  pjss2coi  22744  pj3cor1i  22789  mdexchi  22915  superpos  22934  atcvat4i  22977  mdsymlem3  22985  mdsymlem4  22986  sumdmdii  22995  cdj3lem2b  23017  elabreximd  23039  dftrpred3g  24236  segletr  24737  segleantisym  24738  outsideoftr  24752  domrancur1c  25202  toplat  25290  qusp  25542  trnij  25615  icccon2  25700  ismonc  25814  isepic  25824  idsubfun  25858  exp5d  26208  elicc3  26228  indexa  26412  eldioph2  26841  pell1234qrdich  26946  lnrfg  27323  symggen  27411  climsuselem1  27733  climsuse  27734  stoweidlem29  27778  stoweidlem52  27801  s4f1o  28093  cvrat4  29632  elpaddn0  29989  paddasslem5  30013  paddasslem14  30022  lhprelat3N  30229
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator