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

Theorem exp31 588
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 424 . 2  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
32ex 424 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  exp41  594  exp42  595  expl  602  exbiri  606  anasss  629  an31s  782  3impa  1148  exp516  1173  ax11indalem  2273  ax11inda2ALT  2274  r19.29af2  2840  pwssun  4481  onmindif  4663  ordsucss  4790  tfindsg  4832  mpteqb  5811  dffo3  5876  fconstfv  5946  fliftfun  6026  tfrlem9  6638  oaordi  6781  oaordex  6793  oaass  6796  oarec  6797  omlimcl  6813  omass  6815  oen0  6821  oeordsuc  6829  nnaordi  6853  omsmolem  6888  infensuc  7277  php3  7285  fisucdomOLD  7304  marypha1lem  7430  hartogs  7503  card2on  7512  tz9.12lem3  7705  infxpenlem  7885  cfflb  8129  cfcoflem  8142  cfcof  8144  isf32lem12  8234  zorn2lem6  8371  ondomon  8428  alephval2  8437  pwcfsdom  8448  axrepnd  8459  fpwwe2lem12  8506  genpcd  8873  ltexprlem6  8908  recexsr  8972  axpre-sup  9034  recex  9644  infmrcl  9977  zdiv  10330  uzaddcl  10523  rpnnen1lem5  10594  xrsupsslem  10875  xrinfmsslem  10876  supxrunb1  10888  supxrunb2  10889  elfznelfzo  11182  seqf1o  11354  expcllem  11382  expeq0  11400  mulexp  11409  hashgt12el2  11673  brfi1uzind  11705  s4f1o  11855  cjexp  11945  resqrex  12046  absexp  12099  summo  12501  fsum2d  12545  binom  12599  efexp  12692  demoivreALT  12792  ramcl  13387  ressress  13516  topbas  17027  fctop  17058  cctop  17060  elcls  17127  elcls3  17137  2ndcdisj  17509  filufint  17942  ovoliunlem3  19390  dvge0  19880  ulmcn  20305  usgrares1  21414  cusgrarn  21458  cusgrares  21471  usgrasscusgra  21482  pthdepisspth  21564  fargshiftf1  21614  usgrcyclnl2  21618  constr3trllem2  21628  eupatrl  21680  grpoidinvlem4  21785  grpoinvf  21818  nmosetre  22255  ipasslem1  22322  shmodsi  22881  elspansn5  23066  normcan  23068  h1datomi  23073  nmopsetretALT  23356  nmfnsetre  23370  cnvbraval  23603  opsqrlem1  23633  pjss2coi  23657  pj3cor1i  23702  mdexchi  23828  superpos  23847  atcvat4i  23890  mdsymlem3  23898  mdsymlem4  23899  sumdmdii  23908  cdj3lem2b  23930  elabreximd  23981  iuninc  24001  iundisjf  24019  xrsmulgzz  24190  ofldchr  24234  xrge0iifiso  24311  lmxrge0  24327  esumfzf  24449  sigaclfu2  24494  clim2prod  25206  fprod2d  25295  binomfallfac  25347  faclimlem1  25352  dftrpred3g  25496  segletr  26013  segleantisym  26014  outsideoftr  26028  mblfinlem2  26208  itg2addnc  26222  exp5d  26257  elicc3  26274  indexa  26389  eldioph2  26774  pell1234qrdich  26878  lnrfg  27255  symggen  27343  climsuselem1  27664  climsuse  27665  stoweidlem19  27699  stoweidlem20  27700  stoweidlem27  27707  stoweidlem29  27709  stoweidlem34  27714  stoweidlem35  27715  stoweidlem52  27732  wallispilem3  27747  elfzmlbp  28055  2elfz2melfz  28065  fz0fzelfz0  28066  fz0fzdiffz0  28067  hashimarni  28106  swrdswrd  28129  cshwidx  28172  2cshw1lem1  28178  2cshw1lem2  28179  cshweqrep  28201  cshwssizelem3  28209  usgra2pthspth  28222  usgra2wlkspthlem1  28223  usgra2wlkspth  28225  usgra2adedgspthlem2  28231  usg2wotspth  28268  usgfidegfi  28277  2pthfrgra  28302  3cyclfrgrarn1  28303  3cyclfrgrarn  28304  frgrancvvdeq  28332  frgrancvvdgeq  28333  frgrawopreglem5  28338  usg2spot2nb  28355  cvrat4  30141  elpaddn0  30498  paddasslem5  30522  paddasslem14  30531  lhprelat3N  30738
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 178  df-an 361
  Copyright terms: Public domain W3C validator