MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  exp31 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  2247  ax11inda2ALT  2248  r19.29af2  2808  pwssun  4449  onmindif  4630  ordsucss  4757  tfindsg  4799  mpteqb  5778  dffo3  5843  fconstfv  5913  fliftfun  5993  tfrlem9  6605  oaordi  6748  oaordex  6760  oaass  6763  oarec  6764  omlimcl  6780  omass  6782  oen0  6788  oeordsuc  6796  nnaordi  6820  omsmolem  6855  infensuc  7244  php3  7252  fisucdomOLD  7271  marypha1lem  7396  hartogs  7469  card2on  7478  tz9.12lem3  7671  infxpenlem  7851  cfflb  8095  cfcoflem  8108  cfcof  8110  isf32lem12  8200  zorn2lem6  8337  ondomon  8394  alephval2  8403  pwcfsdom  8414  axrepnd  8425  fpwwe2lem12  8472  genpcd  8839  ltexprlem6  8874  recexsr  8938  axpre-sup  9000  recex  9610  infmrcl  9943  zdiv  10296  uzaddcl  10489  rpnnen1lem5  10560  xrsupsslem  10841  xrinfmsslem  10842  supxrunb1  10854  supxrunb2  10855  elfznelfzo  11147  seqf1o  11319  expcllem  11347  expeq0  11365  mulexp  11374  hashgt12el2  11638  brfi1uzind  11670  s4f1o  11820  cjexp  11910  resqrex  12011  absexp  12064  summo  12466  fsum2d  12510  binom  12564  efexp  12657  demoivreALT  12757  ramcl  13352  ressress  13481  topbas  16992  fctop  17023  cctop  17025  elcls  17092  elcls3  17102  2ndcdisj  17472  filufint  17905  ovoliunlem3  19353  dvge0  19843  ulmcn  20268  usgrares1  21377  cusgrarn  21421  cusgrares  21434  usgrasscusgra  21445  pthdepisspth  21527  fargshiftf1  21577  usgrcyclnl2  21581  constr3trllem2  21591  eupatrl  21643  grpoidinvlem4  21748  grpoinvf  21781  nmosetre  22218  ipasslem1  22285  shmodsi  22844  elspansn5  23029  normcan  23031  h1datomi  23036  nmopsetretALT  23319  nmfnsetre  23333  cnvbraval  23566  opsqrlem1  23596  pjss2coi  23620  pj3cor1i  23665  mdexchi  23791  superpos  23810  atcvat4i  23853  mdsymlem3  23861  mdsymlem4  23862  sumdmdii  23871  cdj3lem2b  23893  elabreximd  23944  iuninc  23964  iundisjf  23982  xrsmulgzz  24153  ofldchr  24197  xrge0iifiso  24274  lmxrge0  24290  esumfzf  24412  sigaclfu2  24457  clim2prod  25169  fprod2d  25258  binomfallfac  25308  faclimlem1  25310  dftrpred3g  25450  segletr  25952  segleantisym  25953  outsideoftr  25967  mblfinlem2  26144  itg2addnc  26158  exp5d  26193  elicc3  26210  indexa  26325  eldioph2  26710  pell1234qrdich  26814  lnrfg  27191  symggen  27279  climsuselem1  27600  climsuse  27601  stoweidlem19  27635  stoweidlem20  27636  stoweidlem27  27643  stoweidlem29  27645  stoweidlem34  27650  stoweidlem35  27651  stoweidlem52  27668  wallispilem3  27683  elfzmlbp  27978  hashimarni  27995  swrdswrd  28011  swrdccatin12lem3a  28021  swrdccatin12lem3  28024  swrdccatin12  28026  swrdccatin12b  28027  swrdccat3  28029  usgra2pthspth  28035  usgra2wlkspthlem1  28036  usgra2wlkspth  28038  usgra2adedgspthlem2  28044  usg2wotspth  28081  usgfidegfi  28090  2pthfrgra  28115  3cyclfrgrarn1  28116  3cyclfrgrarn  28117  frgrancvvdeq  28145  frgrancvvdgeq  28146  frgrawopreglem5  28151  usg2spot2nb  28168  cvrat4  29925  elpaddn0  30282  paddasslem5  30306  paddasslem14  30315  lhprelat3N  30522
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