Theorem exp32 602

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	exp3a 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  610  exp45  611  expr  612  anassrs  643  an13s  796  3impb  1178  ax12eq  2246  ax12el  2247  reusv2lem2  4491  wereu  4712  funfvima3  5951  isomin  6025  isoini  6026  ovg  6228  onint  6405  peano5  6498  tfrlem11  6843  tz7.48lem  6892  oalimcl  6995  oaass  6996  resixpfo  7297  fundmen  7379  php3  7493  ssfi  7529  fodomfi  7586  marypha1lem  7679  card2inf  7766  ixpiunwdom  7802  cantnflt  7876  cantnfltOLD  7906  cnfcom  7929  cnfcomOLD  7937  dfac3  8287  dfac5lem5  8293  dfac5  8294  cfcoflem  8437  fin1a2s  8579  zorn2lem4  8664  zorn2lem7  8667  fpwwe2lem12  8804  wunfi  8884  grur1a  8982  addcanpi  9064  mulcanpi  9065  distrlem1pr  9190  ltaddpr  9199  ltexprlem1  9201  ltexprlem6  9206  ltexprlem7  9207  prodgt0  10170  mulgt1  10184  uzwo  10913  uzwoOLD  10914  xmulasslem  11244  xlemul1a  11247  faclbnd  12062  swrdccatin12lem2a  12372  swrdccat3  12379  cshwidxmod  12436  infpnlem1  13967  isacs4lem  15334  gsmsymgrfixlem1  15925  gsmsymgrfix  15926  dmdprdsplit2lem  16534  pgpfac1  16571  pgpfac  16575  lssssr  17012  islmhm2  17097  lspdisj  17184  cygznlem2a  17959  lindfmm  18215  neindisj  18680  cnpnei  18827  t0dist  18888  ordthauslem  18946  uncmp  18965  fiuncmp  18966  iunconlem  18990  fbasrn  19416  rnelfmlem  19484  rnelfm  19485  fmfnfmlem2  19487  fmfnfmlem4  19489  fclscf  19557  alexsubALTlem3  19580  alexsubALTlem4  19581  alexsubALT  19582  reconn  20364  fsumcn  20405  ovolfiniun  20943  dyadmax  21037  dyadmbllem  21038  dvmptfsum  21406  dvlip2  21426  dvivthlem1  21439  dvcnvrelem1  21448  ply1divex  21567  fta1g  21598  plydivex  21722  fta1  21733  mulcxp  22089  lgsquad2lem2  22657  pntlem3  22817  brbtwn  23080  brcgr  23081  brbtwn2  23086  axeuclid  23144  eupath2  23536  grpoidinvlem3  23628  grpoidinv  23630  shorth  24633  pjhthmo  24640  pjpjpre  24757  elspansn5  24912  lnopmi  25339  adjlnop  25425  leopmul2i  25474  stlesi  25580  ssmd2  25651  dmdsl3  25654  mdexchi  25674  cvexchlem  25707  atcv1  25719  atcvatlem  25724  atabsi  25740  mdsymlem2  25743  mdsymlem3  25744  mdsymlem5  25746  sumdmdii  25754  sumdmdlem  25757  sumdmdlem2  25758  dya2iocnrect  26632  pconcon  27050  iccllyscon  27069  trpredmintr  27624  poseq  27643  nodenselem8  27758  nocvxmin  27761  cgrextend  27968  btwnexch2  27983  colineardim1  28021  lineext  28036  btwnconn1lem13  28059  btwnconn1lem14  28060  seglecgr12im  28070  outsideofeq  28090  outsideofeu  28091  nndivsub  28233  ee7.2aOLD  28237  heicant  28351  nn0prpwlem  28442  neibastop2lem  28506  tailfb  28523  filbcmb  28559  prdsbnd2  28619  heibor  28645  rngoisocnv  28712  mzpcompact2lem  29013  pellfundex  29152  acongsym  29244  pwssplit4  29367  pwslnm  29372  stoweidlem17  29737  f0rn0  30066  elovmpt3rab1  30088  wwlknred  30280  wwlkextinj  30287  clwlkisclwwlklem2a  30372  wwlkext2clwwlk  30390  clwwlkextfrlem1  30594  frgraregord013  30636  lmod0rng  30696  bnj571  31733  pmodlem2  33213  lhpexle3lem  33377  lhpex2leN  33379  cdleme22b  33707  cdleme32d  33810  cdleme32f  33812  trlord  33935  cdlemg1cex  33954  cdlemj2  34188  cdlemk38  34281  cdlemk19x  34309  dihord2pre  34592