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

Theorem exp32 589
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 424 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
32exp3a 426 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  exp44  597  exp45  598  expr  599  anassrs  630  an13s  779  3impb  1149  ax11eq  2243  ax11el  2244  wereu  4538  reusv2lem2  4684  onint  4734  peano5  4827  funfvima3  5934  isomin  6016  isoini  6017  ovg  6171  tfrlem11  6608  tz7.48lem  6657  abianfplem  6674  oalimcl  6762  oaass  6763  resixpfo  7059  fundmen  7139  php3  7252  ssfi  7288  fodomfi  7344  marypha1lem  7396  card2inf  7479  ixpiunwdom  7515  cantnflt  7583  cnfcom  7613  dfac3  7958  dfac5lem5  7964  dfac5  7965  cfcoflem  8108  fin1a2s  8250  zorn2lem4  8335  zorn2lem7  8338  fpwwe2lem12  8472  wunfi  8552  grur1a  8650  addcanpi  8732  mulcanpi  8733  distrlem1pr  8858  ltaddpr  8867  ltexprlem1  8869  ltexprlem6  8874  ltexprlem7  8875  prodgt0  9811  mulgt1  9825  uzwo  10495  uzwoOLD  10496  xmulasslem  10820  xlemul1a  10823  faclbnd  11536  infpnlem1  13233  clatglble  14507  isacs4lem  14549  dmdprdsplit2lem  15558  pgpfac1  15593  pgpfac  15597  lssssr  15984  islmhm2  16069  lspdisj  16152  cygznlem2a  16803  neindisj  17136  cnpnei  17282  t0dist  17343  ordthauslem  17401  uncmp  17420  fiuncmp  17421  iunconlem  17443  fbasrn  17869  rnelfmlem  17937  rnelfm  17938  fmfnfmlem2  17940  fmfnfmlem4  17942  fclscf  18010  alexsubALTlem3  18033  alexsubALTlem4  18034  alexsubALT  18035  reconn  18812  fsumcn  18853  ovolfiniun  19350  dyadmax  19443  dyadmbllem  19444  dvmptfsum  19812  dvlip2  19832  dvivthlem1  19845  dvcnvrelem1  19854  ply1divex  20012  fta1g  20043  plydivex  20167  fta1  20178  mulcxp  20529  lgsquad2lem2  21096  pntlem3  21256  eupath2  21655  grpoidinvlem3  21747  grpoidinv  21749  shorth  22750  pjhthmo  22757  pjpjpre  22874  elspansn5  23029  lnopmi  23456  adjlnop  23542  leopmul2i  23591  stlesi  23697  ssmd2  23768  dmdsl3  23771  mdexchi  23791  cvexchlem  23824  atcv1  23836  atcvatlem  23841  atabsi  23857  mdsymlem2  23860  mdsymlem3  23861  mdsymlem5  23863  sumdmdii  23871  sumdmdlem  23874  sumdmdlem2  23875  dya2iocnrect  24584  pconcon  24871  iccllyscon  24890  trpredmintr  25448  poseq  25467  nodenselem8  25556  nocvxmin  25559  brbtwn  25742  brcgr  25743  brbtwn2  25748  axeuclid  25806  cgrextend  25846  btwnexch2  25861  colineardim1  25899  lineext  25914  btwnconn1lem13  25937  btwnconn1lem14  25938  seglecgr12im  25948  outsideofeq  25968  outsideofeu  25969  nndivsub  26111  ee7.2aOLD  26115  nn0prpwlem  26215  neibastop2lem  26279  tailfb  26296  filbcmb  26332  prdsbnd2  26394  heibor  26420  rngoisocnv  26487  mzpcompact2lem  26698  pellfundex  26839  acongsym  26931  pwssplit4  27059  pwslnm  27064  lindfmm  27165  stoweidlem17  27633  bnj571  28983  pmodlem2  30329  lhpexle3lem  30493  lhpex2leN  30495  cdleme22b  30823  cdleme32d  30926  cdleme32f  30928  trlord  31051  cdlemg1cex  31070  cdlemj2  31304  cdlemk38  31397  cdlemk19x  31425  dihord2pre  31708
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