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  2149  ax11inda2ALT  2150  pwssun  4315  onmindif  4498  ordsucss  4625  tfindsg  4667  mpteqb  5630  dffo3  5691  fconstfv  5750  fliftfun  5827  tfrlem9  6417  oaordi  6560  oaordex  6572  oaass  6575  oarec  6576  omlimcl  6592  omass  6594  oen0  6600  oeordsuc  6608  nnaordi  6632  omsmolem  6667  infensuc  7055  php3  7063  fisucdomOLD  7082  marypha1lem  7202  hartogs  7275  card2on  7284  tz9.12lem3  7477  infxpenlem  7657  cfflb  7901  cfcoflem  7914  cfcof  7916  isf32lem12  8006  zorn2lem6  8144  ondomon  8201  alephval2  8210  pwcfsdom  8221  axrepnd  8232  fpwwe2lem12  8279  genpcd  8646  ltexprlem6  8681  recexsr  8745  axpre-sup  8807  recex  9416  infmrcl  9749  zdiv  10098  uzaddcl  10291  rpnnen1lem5  10362  xrsupsslem  10641  xrinfmsslem  10642  supxrunb1  10654  supxrunb2  10655  seqf1o  11103  expcllem  11130  expeq0  11148  mulexp  11157  cjexp  11651  resqrex  11752  absexp  11805  summo  12206  fsum2d  12250  binom  12304  efexp  12397  demoivreALT  12497  ramcl  13092  ressress  13221  topbas  16726  fctop  16757  cctop  16759  elcls  16826  elcls3  16836  2ndcdisj  17198  filufint  17631  ovoliunlem3  18879  dvge0  19369  ulmcn  19792  grpoidinvlem4  20890  grpoinvf  20923  nmosetre  21358  ipasslem1  21425  shmodsi  21984  elspansn5  22169  normcan  22171  h1datomi  22176  nmopsetretALT  22459  nmfnsetre  22473  cnvbraval  22706  opsqrlem1  22736  pjss2coi  22760  pj3cor1i  22805  mdexchi  22931  superpos  22950  atcvat4i  22993  mdsymlem3  23001  mdsymlem4  23002  sumdmdii  23011  cdj3lem2b  23033  elabreximd  23055  dftrpred3g  24307  segletr  24809  segleantisym  24810  outsideoftr  24824  itg2addnc  25005  domrancur1c  25305  toplat  25393  qusp  25645  trnij  25718  icccon2  25803  ismonc  25917  isepic  25927  idsubfun  25961  exp5d  26311  elicc3  26331  indexa  26515  eldioph2  26944  pell1234qrdich  27049  lnrfg  27426  symggen  27514  climsuselem1  27836  climsuse  27837  stoweidlem29  27881  stoweidlem52  27904  elfznelfzo  28213  hashgt12el2  28219  s4f1o  28225  pthdepisspth  28360  fargshiftf1  28382  eupatrl  28385  usgrcyclnl2  28387  constr3trllem2  28397  3cyclfrgrarn1  28435  3cyclfrgrarn  28436  cvrat4  30254  elpaddn0  30611  paddasslem5  30635  paddasslem14  30644  lhprelat3N  30851
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