Theorem exp32 605

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

Step	Hyp	Ref	Expression
1		exp32.1	. . 3 |- ( ( ph /\ ( ps /\ ch ) ) -> th )
2	1	ex 434	. 2 |- ( ph -> ( ( ps /\ ch ) -> th ) )
3	2	expd 436	1 |- ( ph -> ( ps -> ( ch -> th ) ) )

Syntax hints:   -> wi 4   /\ wa 369

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 185  df-an 371

This theorem is referenced by:  exp44  613  exp45  614  expr  615  anassrs  648  an13s  801  3impb  1183  ax12eq  2242  ax12el  2243  reusv2lem2  4509  wereu  4731  funfvima3  5969  isomin  6043  isoini  6044  ovg  6244  onint  6421  peano5  6514  tfrlem11  6862  tz7.48lem  6911  oalimcl  7014  oaass  7015  resixpfo  7316  fundmen  7398  php3  7512  ssfi  7548  fodomfi  7605  marypha1lem  7698  card2inf  7785  ixpiunwdom  7821  cantnflt  7895  cantnfltOLD  7925  cnfcom  7948  cnfcomOLD  7956  dfac3  8306  dfac5lem5  8312  dfac5  8313  cfcoflem  8456  fin1a2s  8598  zorn2lem4  8683  zorn2lem7  8686  fpwwe2lem12  8823  wunfi  8903  grur1a  9001  addcanpi  9083  mulcanpi  9084  distrlem1pr  9209  ltaddpr  9218  ltexprlem1  9220  ltexprlem6  9225  ltexprlem7  9226  prodgt0  10189  mulgt1  10203  uzwo  10932  uzwoOLD  10933  xmulasslem  11263  xlemul1a  11266  faclbnd  12081  swrdccatin12lem2a  12391  swrdccat3  12398  cshwidxmod  12455  infpnlem1  13986  isacs4lem  15353  gsmsymgrfixlem1  15947  gsmsymgrfix  15948  dmdprdsplit2lem  16559  pgpfac1  16596  pgpfac  16600  lssssr  17049  islmhm2  17134  lspdisj  17221  cygznlem2a  18015  lindfmm  18271  neindisj  18736  cnpnei  18883  t0dist  18944  ordthauslem  19002  uncmp  19021  fiuncmp  19022  iunconlem  19046  fbasrn  19472  rnelfmlem  19540  rnelfm  19541  fmfnfmlem2  19543  fmfnfmlem4  19545  fclscf  19613  alexsubALTlem3  19636  alexsubALTlem4  19637  alexsubALT  19638  reconn  20420  fsumcn  20461  ovolfiniun  20999  dyadmax  21093  dyadmbllem  21094  dvmptfsum  21462  dvlip2  21482  dvivthlem1  21495  dvcnvrelem1  21504  ply1divex  21623  fta1g  21654  plydivex  21778  fta1  21789  mulcxp  22145  lgsquad2lem2  22713  pntlem3  22873  brbtwn  23160  brcgr  23161  brbtwn2  23166  axeuclid  23224  eupath2  23616  grpoidinvlem3  23708  grpoidinv  23710  shorth  24713  pjhthmo  24720  pjpjpre  24837  elspansn5  24992  lnopmi  25419  adjlnop  25505  leopmul2i  25554  stlesi  25660  ssmd2  25731  dmdsl3  25734  mdexchi  25754  cvexchlem  25787  atcv1  25799  atcvatlem  25804  atabsi  25820  mdsymlem2  25823  mdsymlem3  25824  mdsymlem5  25826  sumdmdii  25834  sumdmdlem  25837  sumdmdlem2  25838  dya2iocnrect  26711  pconcon  27135  iccllyscon  27154  trpredmintr  27710  poseq  27729  nodenselem8  27844  nocvxmin  27847  cgrextend  28054  btwnexch2  28069  colineardim1  28107  lineext  28122  btwnconn1lem13  28145  btwnconn1lem14  28146  seglecgr12im  28156  outsideofeq  28176  outsideofeu  28177  nndivsub  28318  ee7.2aOLD  28322  heicant  28445  nn0prpwlem  28536  neibastop2lem  28600  tailfb  28617  filbcmb  28653  prdsbnd2  28713  heibor  28739  rngoisocnv  28806  mzpcompact2lem  29107  pellfundex  29246  acongsym  29338  pwssplit4  29461  pwslnm  29466  stoweidlem17  29831  f0rn0  30160  elovmpt3rab1  30182  wwlknred  30374  wwlkextinj  30381  clwlkisclwwlklem2a  30466  wwlkext2clwwlk  30484  clwwlkextfrlem1  30688  frgraregord013  30730  lmod0rng  30798  bnj571  31918  pmodlem2  33510  lhpexle3lem  33674  lhpex2leN  33676  cdleme22b  34004  cdleme32d  34107  cdleme32f  34109  trlord  34232  cdlemg1cex  34251  cdlemj2  34485  cdlemk38  34578  cdlemk19x  34606  dihord2pre  34889