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

Theorem exp32 590
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 425 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
32exp3a 427 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  exp44  598  exp45  599  expr  600  anassrs  631  an13s  780  3impb  1150  ax11eq  2272  ax11el  2273  wereu  4580  reusv2lem2  4727  onint  4777  peano5  4870  funfvima3  5977  isomin  6059  isoini  6060  ovg  6214  tfrlem11  6651  tz7.48lem  6700  abianfplem  6717  oalimcl  6805  oaass  6806  resixpfo  7102  fundmen  7182  php3  7295  ssfi  7331  fodomfi  7387  marypha1lem  7440  card2inf  7525  ixpiunwdom  7561  cantnflt  7629  cnfcom  7659  dfac3  8004  dfac5lem5  8010  dfac5  8011  cfcoflem  8154  fin1a2s  8296  zorn2lem4  8381  zorn2lem7  8384  fpwwe2lem12  8518  wunfi  8598  grur1a  8696  addcanpi  8778  mulcanpi  8779  distrlem1pr  8904  ltaddpr  8913  ltexprlem1  8915  ltexprlem6  8920  ltexprlem7  8921  prodgt0  9857  mulgt1  9871  uzwo  10541  uzwoOLD  10542  xmulasslem  10866  xlemul1a  10869  faclbnd  11583  infpnlem1  13280  clatglble  14554  isacs4lem  14596  dmdprdsplit2lem  15605  pgpfac1  15640  pgpfac  15644  lssssr  16031  islmhm2  16116  lspdisj  16199  cygznlem2a  16850  neindisj  17183  cnpnei  17330  t0dist  17391  ordthauslem  17449  uncmp  17468  fiuncmp  17469  iunconlem  17492  fbasrn  17918  rnelfmlem  17986  rnelfm  17987  fmfnfmlem2  17989  fmfnfmlem4  17991  fclscf  18059  alexsubALTlem3  18082  alexsubALTlem4  18083  alexsubALT  18084  reconn  18861  fsumcn  18902  ovolfiniun  19399  dyadmax  19492  dyadmbllem  19493  dvmptfsum  19861  dvlip2  19881  dvivthlem1  19894  dvcnvrelem1  19903  ply1divex  20061  fta1g  20092  plydivex  20216  fta1  20227  mulcxp  20578  lgsquad2lem2  21145  pntlem3  21305  eupath2  21704  grpoidinvlem3  21796  grpoidinv  21798  shorth  22799  pjhthmo  22806  pjpjpre  22923  elspansn5  23078  lnopmi  23505  adjlnop  23591  leopmul2i  23640  stlesi  23746  ssmd2  23817  dmdsl3  23820  mdexchi  23840  cvexchlem  23873  atcv1  23885  atcvatlem  23890  atabsi  23906  mdsymlem2  23909  mdsymlem3  23910  mdsymlem5  23912  sumdmdii  23920  sumdmdlem  23923  sumdmdlem2  23924  dya2iocnrect  24633  pconcon  24920  iccllyscon  24939  trpredmintr  25511  poseq  25530  nodenselem8  25645  nocvxmin  25648  brbtwn  25840  brcgr  25841  brbtwn2  25846  axeuclid  25904  cgrextend  25944  btwnexch2  25959  colineardim1  25997  lineext  26012  btwnconn1lem13  26035  btwnconn1lem14  26036  seglecgr12im  26046  outsideofeq  26066  outsideofeu  26067  nndivsub  26209  ee7.2aOLD  26213  nn0prpwlem  26327  neibastop2lem  26391  tailfb  26408  filbcmb  26444  prdsbnd2  26506  heibor  26532  rngoisocnv  26599  mzpcompact2lem  26810  pellfundex  26951  acongsym  27043  pwssplit4  27170  pwslnm  27175  lindfmm  27276  stoweidlem17  27744  f0rn0  28081  swrdccatin12lem3a  28230  swrdccat3  28237  bnj571  29339  pmodlem2  30706  lhpexle3lem  30870  lhpex2leN  30872  cdleme22b  31200  cdleme32d  31303  cdleme32f  31305  trlord  31428  cdlemg1cex  31447  cdlemj2  31681  cdlemk38  31774  cdlemk19x  31802  dihord2pre  32085
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 179  df-an 362
  Copyright terms: Public domain W3C validator