Theorem exp32 614

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

Syntax hints:   -> wi 4   /\ wa 375

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 190  df-an 377

This theorem is referenced by:  exp44  622  exp45  623  expr  624  anassrs  658  an13s  817  3impb  1211  reusv2lem2  4622  wereu  4852  f0rn0  5795  funfvima3  6172  isomin  6258  isoini  6259  ovg  6467  elovmpt3rab1  6559  onint  6654  peano5  6748  tfrlem11  7137  tz7.48lem  7189  oalimcl  7292  oaass  7293  resixpfo  7591  fundmen  7674  php3  7789  ssfi  7823  fodomfi  7881  marypha1lem  7978  card2inf  8101  ixpiunwdom  8137  cantnflt  8208  cnfcom  8236  dfac3  8583  dfac5lem5  8589  dfac5  8590  cfcoflem  8733  fin1a2s  8875  zorn2lem4  8960  zorn2lem7  8963  fpwwe2lem12  9097  wunfi  9177  grur1a  9275  addcanpi  9355  mulcanpi  9356  distrlem1pr  9481  ltaddpr  9490  ltexprlem1  9492  ltexprlem6  9497  ltexprlem7  9498  prodgt0  10483  mulgt1  10497  uzwo  11256  xmulasslem  11605  xlemul1a  11608  faclbnd  12513  swrdccatin12lem2a  12884  swrdccat3  12891  swrdccat  12892  cshwidxmod  12948  infpnlem1  14909  isacs4lem  16469  gsmsymgrfixlem1  17123  gsmsymgrfix  17124  dmdprdsplit2lem  17733  pgpfac1  17768  pgpfac  17772  lssssr  18231  islmhm2  18316  lspdisj  18403  cygznlem2a  19193  lindfmm  19440  scmataddcl  19596  scmatsubcl  19597  scmatmulcl  19598  cayhamlem3  19966  cayleyhamilton1  19971  neindisj  20188  cnpnei  20335  t0dist  20396  ordthauslem  20454  uncmp  20473  fiuncmp  20474  iunconlem  20497  fbasrn  20954  rnelfmlem  21022  rnelfm  21023  fmfnfmlem2  21025  fmfnfmlem4  21027  fclscf  21095  alexsubALTlem3  21119  alexsubALTlem4  21120  alexsubALT  21121  reconn  21901  fsumcn  21957  ovolfiniun  22509  dyadmax  22612  dyadmbllem  22613  dvmptfsum  22983  dvlip2  23003  dvivthlem1  23016  dvcnvrelem1  23025  ply1divex  23143  fta1g  23174  plydivex  23306  fta1  23317  mulcxp  23686  lgsquad2lem2  24343  pntlem3  24503  brbtwn  24985  brcgr  24986  brbtwn2  24991  axeuclid  25049  wwlknred  25507  wwlkextinj  25514  clwlkisclwwlklem2a  25569  wwlkext2clwwlk  25587  eupath2  25764  clwwlkextfrlem1  25860  frgraregord013  25902  grpoidinvlem3  25990  shorth  27004  pjhthmo  27011  pjpjpre  27128  elspansn5  27283  lnopmi  27709  adjlnop  27795  leopmul2i  27844  stlesi  27950  ssmd2  28021  dmdsl3  28024  mdexchi  28044  cvexchlem  28077  atcv1  28089  atcvatlem  28094  atabsi  28110  mdsymlem2  28113  mdsymlem5  28116  sumdmdii  28124  sumdmdlem  28127  sumdmdlem2  28128  dya2iocnrect  29153  bnj571  29767  pconcon  30004  iccllyscon  30023  trpredmintr  30522  poseq  30541  nodenselem8  30627  nocvxmin  30630  cgrextend  30825  btwnexch2  30840  colineardim1  30878  lineext  30893  btwnconn1lem13  30916  btwnconn1lem14  30917  seglecgr12im  30927  outsideofeq  30947  outsideofeu  30948  nn0prpwlem  31028  neibastop2lem  31066  tailfb  31083  nndivsub  31167  ee7.2aOLD  31171  poimirlem31  32017  heicant  32021  filbcmb  32113  prdsbnd2  32173  heibor  32199  rngoisocnv  32266  ax12eq  32558  ax12el  32559  pmodlem2  33458  cdleme22b  33954  cdleme32d  34057  cdleme32f  34059  trlord  34182  cdlemj2  34435  cdlemk38  34528  cdlemk19x  34556  dihord2pre  34839  mzpcompact2lem  35639  pellfundex  35780  acongsym  35872  pwssplit4  35993  pwslnm  35998  relexpmulg  36348  stoweidlem17  37978  iccpartigtl  38872  bgoldbtbndlem2  39036  bgoldbtbndlem3  39037  bgoldbtbnd  39039  pfxccat3  39104  uhgr1wlkspthlem2  39882  umgr2wlk  39994  lmod0rng  40237  2zrngamgm  40308