Theorem exp32 603

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

Syntax hints:   -> wi 4   /\ wa 367

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 369

This theorem is referenced by:  exp44  611  exp45  612  expr  613  anassrs  646  an13s  801  3impb  1190  reusv2lem2  4567  wereu  4789  f0rn0  5678  funfvima3  6050  isomin  6134  isoini  6135  ovg  6340  elovmpt3rab1  6435  onint  6529  peano5  6622  tfrlem11  6975  tz7.48lem  7024  oalimcl  7127  oaass  7128  resixpfo  7426  fundmen  7508  php3  7622  ssfi  7656  fodomfi  7714  marypha1lem  7808  card2inf  7896  ixpiunwdom  7932  cantnflt  8004  cantnfltOLD  8034  cnfcom  8057  cnfcomOLD  8065  dfac3  8415  dfac5lem5  8421  dfac5  8422  cfcoflem  8565  fin1a2s  8707  zorn2lem4  8792  zorn2lem7  8795  fpwwe2lem12  8930  wunfi  9010  grur1a  9108  addcanpi  9188  mulcanpi  9189  distrlem1pr  9314  ltaddpr  9323  ltexprlem1  9325  ltexprlem6  9330  ltexprlem7  9331  prodgt0  10304  mulgt1  10318  uzwo  11064  xmulasslem  11398  xlemul1a  11401  faclbnd  12270  swrdccatin12lem2a  12621  swrdccat3  12628  swrdccat  12629  cshwidxmod  12685  infpnlem1  14430  isacs4lem  15915  gsmsymgrfixlem1  16569  gsmsymgrfix  16570  dmdprdsplit2lem  17207  pgpfac1  17244  pgpfac  17248  lssssr  17712  islmhm2  17797  lspdisj  17884  cygznlem2a  18697  lindfmm  18947  scmataddcl  19103  scmatsubcl  19104  scmatmulcl  19105  cayhamlem3  19473  cayleyhamilton1  19478  neindisj  19704  cnpnei  19851  t0dist  19912  ordthauslem  19970  uncmp  19989  fiuncmp  19990  iunconlem  20013  fbasrn  20470  rnelfmlem  20538  rnelfm  20539  fmfnfmlem2  20541  fmfnfmlem4  20543  fclscf  20611  alexsubALTlem3  20634  alexsubALTlem4  20635  alexsubALT  20636  reconn  21418  fsumcn  21459  ovolfiniun  21997  dyadmax  22092  dyadmbllem  22093  dvmptfsum  22461  dvlip2  22481  dvivthlem1  22494  dvcnvrelem1  22503  ply1divex  22622  fta1g  22653  plydivex  22778  fta1  22789  mulcxp  23153  lgsquad2lem2  23751  pntlem3  23911  brbtwn  24323  brcgr  24324  brbtwn2  24329  axeuclid  24387  wwlknred  24844  wwlkextinj  24851  clwlkisclwwlklem2a  24906  wwlkext2clwwlk  24924  eupath2  25101  clwwlkextfrlem1  25197  frgraregord013  25239  grpoidinvlem3  25325  shorth  26330  pjhthmo  26337  pjpjpre  26454  elspansn5  26609  lnopmi  27035  adjlnop  27121  leopmul2i  27170  stlesi  27276  ssmd2  27347  dmdsl3  27350  mdexchi  27370  cvexchlem  27403  atcv1  27415  atcvatlem  27420  atabsi  27436  mdsymlem2  27439  mdsymlem5  27442  sumdmdii  27450  sumdmdlem  27453  sumdmdlem2  27454  dya2iocnrect  28408  pconcon  28865  iccllyscon  28884  trpredmintr  29479  poseq  29498  nodenselem8  29613  nocvxmin  29616  cgrextend  29811  btwnexch2  29826  colineardim1  29864  lineext  29879  btwnconn1lem13  29902  btwnconn1lem14  29903  seglecgr12im  29913  outsideofeq  29933  outsideofeu  29934  nndivsub  30075  ee7.2aOLD  30079  heicant  30214  nn0prpwlem  30306  neibastop2lem  30344  tailfb  30361  filbcmb  30397  prdsbnd2  30457  heibor  30483  rngoisocnv  30550  mzpcompact2lem  30849  pellfundex  30987  acongsym  31079  pwssplit4  31201  pwslnm  31206  stoweidlem17  31965  pfxccat3  32601  lmod0rng  32874  2zrngamgm  32945  bnj571  34311  ax12eq  35084  ax12el  35085  pmodlem2  35984  cdleme22b  36480  cdleme32d  36583  cdleme32f  36585  trlord  36708  cdlemj2  36961  cdlemk38  37054  cdlemk19x  37082  dihord2pre  37365  relexpmulg  38246