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

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

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  4627  wereu  4850  f0rn0  5785  funfvima3  6157  isomin  6243  isoini  6244  ovg  6449  elovmpt3rab1  6541  onint  6636  peano5  6730  tfrlem11  7114  tz7.48lem  7166  oalimcl  7269  oaass  7270  resixpfo  7568  fundmen  7650  php3  7764  ssfi  7798  fodomfi  7856  marypha1lem  7953  card2inf  8070  ixpiunwdom  8106  cantnflt  8176  cnfcom  8204  dfac3  8550  dfac5lem5  8556  dfac5  8557  cfcoflem  8700  fin1a2s  8842  zorn2lem4  8927  zorn2lem7  8930  fpwwe2lem12  9065  wunfi  9145  grur1a  9243  addcanpi  9323  mulcanpi  9324  distrlem1pr  9449  ltaddpr  9458  ltexprlem1  9460  ltexprlem6  9465  ltexprlem7  9466  prodgt0  10449  mulgt1  10463  uzwo  11222  xmulasslem  11571  xlemul1a  11574  faclbnd  12472  swrdccatin12lem2a  12826  swrdccat3  12833  swrdccat  12834  cshwidxmod  12890  infpnlem1  14808  isacs4lem  16356  gsmsymgrfixlem1  17010  gsmsymgrfix  17011  dmdprdsplit2lem  17604  pgpfac1  17639  pgpfac  17643  lssssr  18102  islmhm2  18187  lspdisj  18274  cygznlem2a  19060  lindfmm  19307  scmataddcl  19463  scmatsubcl  19464  scmatmulcl  19465  cayhamlem3  19833  cayleyhamilton1  19838  neindisj  20055  cnpnei  20202  t0dist  20263  ordthauslem  20321  uncmp  20340  fiuncmp  20341  iunconlem  20364  fbasrn  20821  rnelfmlem  20889  rnelfm  20890  fmfnfmlem2  20892  fmfnfmlem4  20894  fclscf  20962  alexsubALTlem3  20986  alexsubALTlem4  20987  alexsubALT  20988  reconn  21748  fsumcn  21789  ovolfiniun  22323  dyadmax  22424  dyadmbllem  22425  dvmptfsum  22795  dvlip2  22815  dvivthlem1  22828  dvcnvrelem1  22837  ply1divex  22953  fta1g  22984  plydivex  23109  fta1  23120  mulcxp  23486  lgsquad2lem2  24141  pntlem3  24301  brbtwn  24766  brcgr  24767  brbtwn2  24772  axeuclid  24830  wwlknred  25287  wwlkextinj  25294  clwlkisclwwlklem2a  25349  wwlkext2clwwlk  25367  eupath2  25544  clwwlkextfrlem1  25640  frgraregord013  25682  grpoidinvlem3  25770  shorth  26774  pjhthmo  26781  pjpjpre  26898  elspansn5  27053  lnopmi  27479  adjlnop  27565  leopmul2i  27614  stlesi  27720  ssmd2  27791  dmdsl3  27794  mdexchi  27814  cvexchlem  27847  atcv1  27859  atcvatlem  27864  atabsi  27880  mdsymlem2  27883  mdsymlem5  27886  sumdmdii  27894  sumdmdlem  27897  sumdmdlem2  27898  dya2iocnrect  28933  bnj571  29496  pconcon  29733  iccllyscon  29752  trpredmintr  30250  poseq  30269  nodenselem8  30353  nocvxmin  30356  cgrextend  30551  btwnexch2  30566  colineardim1  30604  lineext  30619  btwnconn1lem13  30642  btwnconn1lem14  30643  seglecgr12im  30653  outsideofeq  30673  outsideofeu  30674  nn0prpwlem  30754  neibastop2lem  30792  tailfb  30809  nndivsub  30893  ee7.2aOLD  30897  poimirlem31  31665  heicant  31669  filbcmb  31761  prdsbnd2  31821  heibor  31847  rngoisocnv  31914  ax12eq  32211  ax12el  32212  pmodlem2  33111  cdleme22b  33607  cdleme32d  33710  cdleme32f  33712  trlord  33835  cdlemj2  34088  cdlemk38  34181  cdlemk19x  34209  dihord2pre  34492  mzpcompact2lem  35292  pellfundex  35430  acongsym  35522  pwssplit4  35643  pwslnm  35648  relexpmulg  35931  stoweidlem17  37436  iccpartigtl  38117  bgoldbtbndlem2  38281  bgoldbtbndlem3  38282  bgoldbtbnd  38284  pfxccat3  38347  lmod0rng  38616  2zrngamgm  38687