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

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

Proof of Theorem exp32
StepHypRef Expression
1 exp32.1 . . 3  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
21ex 435 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
32expd 437 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  exp44  616  exp45  617  expr  618  anassrs  652  an13s  810  3impb  1201  reusv2lem2  4626  wereu  4849  f0rn0  5785  funfvima3  6157  isomin  6243  isoini  6244  ovg  6449  elovmpt3rab1  6541  onint  6636  peano5  6730  tfrlem11  7117  tz7.48lem  7169  oalimcl  7272  oaass  7273  resixpfo  7571  fundmen  7653  php3  7767  ssfi  7801  fodomfi  7859  marypha1lem  7956  card2inf  8079  ixpiunwdom  8115  cantnflt  8185  cnfcom  8213  dfac3  8559  dfac5lem5  8565  dfac5  8566  cfcoflem  8709  fin1a2s  8851  zorn2lem4  8936  zorn2lem7  8939  fpwwe2lem12  9073  wunfi  9153  grur1a  9251  addcanpi  9331  mulcanpi  9332  distrlem1pr  9457  ltaddpr  9466  ltexprlem1  9468  ltexprlem6  9473  ltexprlem7  9474  prodgt0  10457  mulgt1  10471  uzwo  11229  xmulasslem  11578  xlemul1a  11581  faclbnd  12481  swrdccatin12lem2a  12843  swrdccat3  12850  swrdccat  12851  cshwidxmod  12907  infpnlem1  14853  isacs4lem  16413  gsmsymgrfixlem1  17067  gsmsymgrfix  17068  dmdprdsplit2lem  17677  pgpfac1  17712  pgpfac  17716  lssssr  18175  islmhm2  18260  lspdisj  18347  cygznlem2a  19136  lindfmm  19383  scmataddcl  19539  scmatsubcl  19540  scmatmulcl  19541  cayhamlem3  19909  cayleyhamilton1  19914  neindisj  20131  cnpnei  20278  t0dist  20339  ordthauslem  20397  uncmp  20416  fiuncmp  20417  iunconlem  20440  fbasrn  20897  rnelfmlem  20965  rnelfm  20966  fmfnfmlem2  20968  fmfnfmlem4  20970  fclscf  21038  alexsubALTlem3  21062  alexsubALTlem4  21063  alexsubALT  21064  reconn  21844  fsumcn  21900  ovolfiniun  22452  dyadmax  22554  dyadmbllem  22555  dvmptfsum  22925  dvlip2  22945  dvivthlem1  22958  dvcnvrelem1  22967  ply1divex  23085  fta1g  23116  plydivex  23248  fta1  23259  mulcxp  23628  lgsquad2lem2  24285  pntlem3  24445  brbtwn  24927  brcgr  24928  brbtwn2  24933  axeuclid  24991  wwlknred  25449  wwlkextinj  25456  clwlkisclwwlklem2a  25511  wwlkext2clwwlk  25529  eupath2  25706  clwwlkextfrlem1  25802  frgraregord013  25844  grpoidinvlem3  25932  shorth  26946  pjhthmo  26953  pjpjpre  27070  elspansn5  27225  lnopmi  27651  adjlnop  27737  leopmul2i  27786  stlesi  27892  ssmd2  27963  dmdsl3  27966  mdexchi  27986  cvexchlem  28019  atcv1  28031  atcvatlem  28036  atabsi  28052  mdsymlem2  28055  mdsymlem5  28058  sumdmdii  28066  sumdmdlem  28069  sumdmdlem2  28070  dya2iocnrect  29111  bnj571  29725  pconcon  29962  iccllyscon  29981  trpredmintr  30479  poseq  30498  nodenselem8  30582  nocvxmin  30585  cgrextend  30780  btwnexch2  30795  colineardim1  30833  lineext  30848  btwnconn1lem13  30871  btwnconn1lem14  30872  seglecgr12im  30882  outsideofeq  30902  outsideofeu  30903  nn0prpwlem  30983  neibastop2lem  31021  tailfb  31038  nndivsub  31122  ee7.2aOLD  31126  poimirlem31  31935  heicant  31939  filbcmb  32031  prdsbnd2  32091  heibor  32117  rngoisocnv  32184  ax12eq  32481  ax12el  32482  pmodlem2  33381  cdleme22b  33877  cdleme32d  33980  cdleme32f  33982  trlord  34105  cdlemj2  34358  cdlemk38  34451  cdlemk19x  34479  dihord2pre  34762  mzpcompact2lem  35562  pellfundex  35704  acongsym  35796  pwssplit4  35917  pwslnm  35922  relexpmulg  36272  stoweidlem17  37817  iccpartigtl  38607  bgoldbtbndlem2  38771  bgoldbtbndlem3  38772  bgoldbtbnd  38774  pfxccat3  38837  lmod0rng  39488  2zrngamgm  39559
  Copyright terms: Public domain W3C validator