Theorem exp32 631

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 450	. 2 |- ( ph -> ( ( ps /\ ch ) -> th ) )
3	2	expd 452	1 |- ( ph -> ( ps -> ( ch -> th ) ) )

Syntax hints:   -> wi 4   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  exp44  641  exp45  642  expr  643  anassrs  680  an13s  845  3impb  1260  reusv2lem2OLD  4870  wereu  5110  f0rn0  6090  funfvima3  6495  isomin  6587  isoini  6588  ovg  6799  elovmpt3rab1  6893  onint  6995  peano5  7089  tfrlem11  7484  tz7.48lem  7536  oalimcl  7640  oaass  7641  resixpfo  7946  fundmen  8030  php3  8146  ssfi  8180  fodomfi  8239  marypha1lem  8339  card2inf  8460  ixpiunwdom  8496  cantnflt  8569  cnfcom  8597  dfac3  8944  dfac5lem5  8950  dfac5  8951  cfcoflem  9094  fin1a2s  9236  zorn2lem4  9321  zorn2lem7  9324  fpwwe2lem12  9463  wunfi  9543  grur1a  9641  addcanpi  9721  mulcanpi  9722  distrlem1pr  9847  ltaddpr  9856  ltexprlem1  9858  ltexprlem6  9863  ltexprlem7  9864  prodgt0  10868  mulgt1  10882  uzwo  11751  xmulasslem  12115  xlemul1a  12118  faclbnd  13077  swrdccatin12lem2a  13485  swrdccat3  13492  swrdccat  13493  cshwidxmod  13549  s3iunsndisj  13707  dvdsaddre2b  15029  divgcdcoprm0  15379  cncongr2  15382  infpnlem1  15614  isacs4lem  17168  gsmsymgrfixlem1  17847  gsmsymgrfix  17848  dmdprdsplit2lem  18444  pgpfac1  18479  pgpfac  18483  lssssr  18953  islmhm2  19038  lspdisj  19125  cygznlem2a  19916  lindfmm  20166  scmataddcl  20322  scmatsubcl  20323  scmatmulcl  20324  cayhamlem3  20692  cayleyhamilton1  20697  neindisj  20921  cnpnei  21068  t0dist  21129  ordthauslem  21187  uncmp  21206  fiuncmp  21207  iunconnlem  21230  fbasrn  21688  rnelfmlem  21756  rnelfm  21757  fmfnfmlem2  21759  fmfnfmlem4  21761  fclscf  21829  alexsubALTlem3  21853  alexsubALTlem4  21854  alexsubALT  21855  reconn  22631  fsumcn  22673  ovolfiniun  23269  dyadmax  23366  dyadmbllem  23367  dvmptfsum  23738  dvlip2  23758  dvivthlem1  23771  dvcnvrelem1  23780  ply1divex  23896  fta1g  23927  plydivex  24052  fta1  24063  mulcxp  24431  zabsle1  25021  lgsquad2lem2  25110  2lgsoddprm  25141  pntlem3  25298  brbtwn  25779  brcgr  25780  brbtwn2  25785  axeuclid  25843  finsumvtxdg2size  26446  uhgrwkspthlem2  26650  crctcshwlkn0  26713  wwlksnred  26787  wwlksnextinj  26794  wspthsnwspthsnon  26811  umgr2wlk  26845  elwwlks2  26861  clwlkclwwlklem2a  26899  wwlksext2clwwlk  26924  eupth2lems  27098  clwwlkextfrlem1  27208  frgrregord013  27253  grpoidinvlem3  27360  shorth  28154  pjhthmo  28161  pjpjpre  28278  elspansn5  28433  lnopmi  28859  adjlnop  28945  leopmul2i  28994  stlesi  29100  ssmd2  29171  dmdsl3  29174  mdexchi  29194  cvexchlem  29227  atcv1  29239  atcvatlem  29244  atabsi  29260  mdsymlem2  29263  mdsymlem5  29266  sumdmdii  29274  sumdmdlem  29277  sumdmdlem2  29278  dya2iocnrect  30343  bnj571  30976  pconnconn  31213  iccllysconn  31232  trpredmintr  31731  poseq  31750  nodenselem8  31841  nocvxmin  31894  cgrextend  32115  btwnexch2  32130  colineardim1  32168  lineext  32183  btwnconn1lem13  32206  btwnconn1lem14  32207  seglecgr12im  32217  outsideofeq  32237  outsideofeu  32238  nn0prpwlem  32317  neibastop2lem  32355  tailfb  32372  nndivsub  32456  ee7.2aOLD  32460  poimirlem31  33440  heicant  33444  filbcmb  33535  prdsbnd2  33594  heibor  33620  rngoisocnv  33780  ax12eq  34226  ax12el  34227  pmodlem2  35133  cdleme22b  35629  cdleme32d  35732  cdleme32f  35734  trlord  35857  cdlemj2  36110  cdlemk38  36203  cdlemk19x  36231  dihord2pre  36514  mzpcompact2lem  37314  pellfundex  37450  acongsym  37543  pwssplit4  37659  pwslnm  37664  relexpmulg  38002  stoweidlem17  40234  iccpartigtl  41359  pfxccat3  41426  fmtnofac2lem  41480  2pwp1prmfmtno  41504  lighneallem4  41527  bgoldbtbndlem2  41694  bgoldbtbndlem3  41695  bgoldbtbnd  41697  lmod0rng  41868  2zrngamgm  41939