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  803  3impb  1193  ax12eq  2257  ax12el  2258  reusv2lem2  4639  wereu  4865  f0rn0  5760  funfvima3  6134  isomin  6218  isoini  6219  ovg  6426  elovmpt3rab1  6521  onint  6615  peano5  6708  tfrlem11  7059  tz7.48lem  7108  oalimcl  7211  oaass  7212  resixpfo  7509  fundmen  7591  php3  7705  ssfi  7742  fodomfi  7801  marypha1lem  7895  card2inf  7984  ixpiunwdom  8020  cantnflt  8094  cantnfltOLD  8124  cnfcom  8147  cnfcomOLD  8155  dfac3  8505  dfac5lem5  8511  dfac5  8512  cfcoflem  8655  fin1a2s  8797  zorn2lem4  8882  zorn2lem7  8885  fpwwe2lem12  9022  wunfi  9102  grur1a  9200  addcanpi  9280  mulcanpi  9281  distrlem1pr  9406  ltaddpr  9415  ltexprlem1  9417  ltexprlem6  9422  ltexprlem7  9423  prodgt0  10394  mulgt1  10408  uzwo  11155  uzwoOLD  11156  xmulasslem  11488  xlemul1a  11491  faclbnd  12350  swrdccatin12lem2a  12692  swrdccat3  12699  swrdccat  12700  cshwidxmod  12756  infpnlem1  14410  isacs4lem  15777  gsmsymgrfixlem1  16431  gsmsymgrfix  16432  dmdprdsplit2lem  17073  pgpfac1  17110  pgpfac  17114  lssssr  17578  islmhm2  17663  lspdisj  17750  cygznlem2a  18584  lindfmm  18840  scmataddcl  18996  scmatsubcl  18997  scmatmulcl  18998  cayhamlem3  19366  cayleyhamilton1  19371  neindisj  19596  cnpnei  19743  t0dist  19804  ordthauslem  19862  uncmp  19881  fiuncmp  19882  iunconlem  19906  fbasrn  20363  rnelfmlem  20431  rnelfm  20432  fmfnfmlem2  20434  fmfnfmlem4  20436  fclscf  20504  alexsubALTlem3  20527  alexsubALTlem4  20528  alexsubALT  20529  reconn  21311  fsumcn  21352  ovolfiniun  21890  dyadmax  21985  dyadmbllem  21986  dvmptfsum  22354  dvlip2  22374  dvivthlem1  22387  dvcnvrelem1  22396  ply1divex  22515  fta1g  22546  plydivex  22671  fta1  22682  mulcxp  23044  lgsquad2lem2  23612  pntlem3  23772  brbtwn  24180  brcgr  24181  brbtwn2  24186  axeuclid  24244  wwlknred  24701  wwlkextinj  24708  clwlkisclwwlklem2a  24763  wwlkext2clwwlk  24781  eupath2  24958  clwwlkextfrlem1  25054  frgraregord013  25096  grpoidinvlem3  25186  shorth  26191  pjhthmo  26198  pjpjpre  26315  elspansn5  26470  lnopmi  26897  adjlnop  26983  leopmul2i  27032  stlesi  27138  ssmd2  27209  dmdsl3  27212  mdexchi  27232  cvexchlem  27265  atcv1  27277  atcvatlem  27282  atabsi  27298  mdsymlem2  27301  mdsymlem5  27304  sumdmdii  27312  sumdmdlem  27315  sumdmdlem2  27316  dya2iocnrect  28230  pconcon  28654  iccllyscon  28673  trpredmintr  29290  poseq  29309  nodenselem8  29424  nocvxmin  29427  cgrextend  29634  btwnexch2  29649  colineardim1  29687  lineext  29702  btwnconn1lem13  29725  btwnconn1lem14  29726  seglecgr12im  29736  outsideofeq  29756  outsideofeu  29757  nndivsub  29898  ee7.2aOLD  29902  heicant  30025  nn0prpwlem  30116  neibastop2lem  30154  tailfb  30171  filbcmb  30207  prdsbnd2  30267  heibor  30293  rngoisocnv  30360  mzpcompact2lem  30660  pellfundex  30798  acongsym  30890  pwssplit4  31011  pwslnm  31016  stoweidlem17  31753  2zrngamgm  32572  lmod0rng  32829  bnj571  33832  pmodlem2  35446  cdleme22b  35942  cdleme32d  36045  cdleme32f  36047  trlord  36170  cdlemj2  36423  cdlemk38  36516  cdlemk19x  36544  dihord2pre  36827