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  801  3impb  1192  ax12eq  2264  ax12el  2265  reusv2lem2  4649  wereu  4875  f0rn0  5768  funfvima3  6135  isomin  6219  isoini  6220  ovg  6423  elovmpt3rab1  6518  onint  6608  peano5  6701  tfrlem11  7054  tz7.48lem  7103  oalimcl  7206  oaass  7207  resixpfo  7504  fundmen  7586  php3  7700  ssfi  7737  fodomfi  7795  marypha1lem  7889  card2inf  7977  ixpiunwdom  8013  cantnflt  8087  cantnfltOLD  8117  cnfcom  8140  cnfcomOLD  8148  dfac3  8498  dfac5lem5  8504  dfac5  8505  cfcoflem  8648  fin1a2s  8790  zorn2lem4  8875  zorn2lem7  8878  fpwwe2lem12  9015  wunfi  9095  grur1a  9193  addcanpi  9273  mulcanpi  9274  distrlem1pr  9399  ltaddpr  9408  ltexprlem1  9410  ltexprlem6  9415  ltexprlem7  9416  prodgt0  10383  mulgt1  10397  uzwo  11140  uzwoOLD  11141  xmulasslem  11473  xlemul1a  11476  faclbnd  12332  swrdccatin12lem2a  12669  swrdccat3  12676  cshwidxmod  12733  infpnlem1  14283  isacs4lem  15651  gsmsymgrfixlem1  16247  gsmsymgrfix  16248  dmdprdsplit2lem  16884  pgpfac1  16921  pgpfac  16925  lssssr  17382  islmhm2  17467  lspdisj  17554  cygznlem2a  18373  lindfmm  18629  scmataddcl  18785  scmatsubcl  18786  scmatmulcl  18787  cayhamlem3  19155  cayleyhamilton1  19160  neindisj  19384  cnpnei  19531  t0dist  19592  ordthauslem  19650  uncmp  19669  fiuncmp  19670  iunconlem  19694  fbasrn  20120  rnelfmlem  20188  rnelfm  20189  fmfnfmlem2  20191  fmfnfmlem4  20193  fclscf  20261  alexsubALTlem3  20284  alexsubALTlem4  20285  alexsubALT  20286  reconn  21068  fsumcn  21109  ovolfiniun  21647  dyadmax  21742  dyadmbllem  21743  dvmptfsum  22111  dvlip2  22131  dvivthlem1  22144  dvcnvrelem1  22153  ply1divex  22272  fta1g  22303  plydivex  22427  fta1  22438  mulcxp  22794  lgsquad2lem2  23362  pntlem3  23522  brbtwn  23878  brcgr  23879  brbtwn2  23884  axeuclid  23942  wwlknred  24399  wwlkextinj  24406  clwlkisclwwlklem2a  24461  wwlkext2clwwlk  24479  eupath2  24656  clwwlkextfrlem1  24753  frgraregord013  24795  grpoidinvlem3  24884  grpoidinv  24886  shorth  25889  pjhthmo  25896  pjpjpre  26013  elspansn5  26168  lnopmi  26595  adjlnop  26681  leopmul2i  26730  stlesi  26836  ssmd2  26907  dmdsl3  26910  mdexchi  26930  cvexchlem  26963  atcv1  26975  atcvatlem  26980  atabsi  26996  mdsymlem2  26999  mdsymlem3  27000  mdsymlem5  27002  sumdmdii  27010  sumdmdlem  27013  sumdmdlem2  27014  dya2iocnrect  27892  pconcon  28316  iccllyscon  28335  trpredmintr  28891  poseq  28910  nodenselem8  29025  nocvxmin  29028  cgrextend  29235  btwnexch2  29250  colineardim1  29288  lineext  29303  btwnconn1lem13  29326  btwnconn1lem14  29327  seglecgr12im  29337  outsideofeq  29357  outsideofeu  29358  nndivsub  29499  ee7.2aOLD  29503  heicant  29626  nn0prpwlem  29717  neibastop2lem  29781  tailfb  29798  filbcmb  29834  prdsbnd2  29894  heibor  29920  rngoisocnv  29987  mzpcompact2lem  30288  pellfundex  30426  acongsym  30518  pwssplit4  30639  pwslnm  30644  stoweidlem17  31317  lmod0rng  32032  bnj571  33043  pmodlem2  34643  lhpexle3lem  34807  lhpex2leN  34809  cdleme22b  35137  cdleme32d  35240  cdleme32f  35242  trlord  35365  cdlemg1cex  35384  cdlemj2  35618  cdlemk38  35711  cdlemk19x  35739  dihord2pre  36022