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

Theorem exp31 589
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 425 . 2  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
32ex 425 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  exp41  595  exp42  596  expl  603  exbiri  607  anasss  630  an31s  783  3impa  1149  exp516  1174  ax11indalem  2276  ax11inda2ALT  2277  r19.29af2  2850  pwssun  4492  onmindif  4674  ordsucss  4801  tfindsg  4843  mpteqb  5822  dffo3  5887  fconstfv  5957  fliftfun  6037  tfrlem9  6649  oaordi  6792  oaordex  6804  oaass  6807  oarec  6808  omlimcl  6824  omass  6826  oen0  6832  oeordsuc  6840  nnaordi  6864  omsmolem  6899  infensuc  7288  php3  7296  fisucdomOLD  7315  marypha1lem  7441  hartogs  7516  card2on  7525  tz9.12lem3  7718  infxpenlem  7900  cfflb  8144  cfcoflem  8157  cfcof  8159  isf32lem12  8249  zorn2lem6  8386  ondomon  8443  alephval2  8452  pwcfsdom  8463  axrepnd  8474  fpwwe2lem12  8521  genpcd  8888  ltexprlem6  8923  recexsr  8987  axpre-sup  9049  recex  9659  infmrcl  9992  zdiv  10345  uzaddcl  10538  rpnnen1lem5  10609  xrsupsslem  10890  xrinfmsslem  10891  supxrunb1  10903  supxrunb2  10904  elfznelfzo  11197  seqf1o  11369  expcllem  11397  expeq0  11415  mulexp  11424  hashgt12el2  11688  brfi1uzind  11720  s4f1o  11870  cjexp  11960  resqrex  12061  absexp  12114  summo  12516  fsum2d  12560  binom  12614  efexp  12707  demoivreALT  12807  ramcl  13402  ressress  13531  topbas  17042  fctop  17073  cctop  17075  elcls  17142  elcls3  17152  2ndcdisj  17524  filufint  17957  ovoliunlem3  19405  dvge0  19895  ulmcn  20320  usgrares1  21429  cusgrarn  21473  cusgrares  21486  usgrasscusgra  21497  pthdepisspth  21579  fargshiftf1  21629  usgrcyclnl2  21633  constr3trllem2  21643  eupatrl  21695  grpoidinvlem4  21800  grpoinvf  21833  nmosetre  22270  ipasslem1  22337  shmodsi  22896  elspansn5  23081  normcan  23083  h1datomi  23088  nmopsetretALT  23371  nmfnsetre  23385  cnvbraval  23618  opsqrlem1  23648  pjss2coi  23672  pj3cor1i  23717  mdexchi  23843  superpos  23862  atcvat4i  23905  mdsymlem3  23913  mdsymlem4  23914  sumdmdii  23923  cdj3lem2b  23945  elabreximd  23996  iuninc  24016  iundisjf  24034  xrsmulgzz  24205  ofldchr  24249  xrge0iifiso  24326  lmxrge0  24342  esumfzf  24464  sigaclfu2  24509  clim2prod  25221  fprod2d  25310  binomfallfac  25362  faclimlem1  25367  dftrpred3g  25516  segletr  26053  segleantisym  26054  outsideoftr  26068  mblfinlem3  26257  itg2addnc  26273  exp5d  26317  elicc3  26334  indexa  26449  eldioph2  26834  pell1234qrdich  26938  lnrfg  27314  symggen  27402  climsuselem1  27723  climsuse  27724  stoweidlem19  27758  stoweidlem20  27759  stoweidlem27  27766  stoweidlem29  27768  stoweidlem34  27773  stoweidlem35  27774  stoweidlem52  27791  wallispilem3  27806  elfzmlbp  28130  2elfz2melfz  28140  fz0fzelfz0  28141  fz0fzdiffz0  28142  hashimarni  28187  swrdswrd  28233  cshwidx  28276  2cshw1lem1  28282  2cshw1lem2  28283  cshweqrep  28308  cshwssizelem3  28316  usgra2pthspth  28343  usgra2wlkspthlem1  28344  usgra2wlkspth  28346  usgra2adedgspthlem2  28352  wlkiswwlk1  28372  usg2wotspth  28416  usgfidegfi  28425  usgravd00  28436  2pthfrgra  28475  3cyclfrgrarn1  28476  3cyclfrgrarn  28477  frgrancvvdeq  28505  frgrancvvdgeq  28506  frgrawopreglem5  28511  usg2spot2nb  28528  cvrat4  30314  elpaddn0  30671  paddasslem5  30695  paddasslem14  30704  lhprelat3N  30911
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 179  df-an 362
  Copyright terms: Public domain W3C validator