Theorem expd 452

Description: Exportation deduction. (Contributed by NM, 20-Aug-1993.)

Hypothesis

Ref	Expression
expd.1	|- ( ph -> ( ( ps /\ ch ) -> th ) )

Assertion

Ref	Expression
expd	|- ( ph -> ( ps -> ( ch -> th ) ) )

Proof of Theorem expd

Step	Hyp	Ref	Expression
1		expd.1	. . . 4 |- ( ph -> ( ( ps /\ ch ) -> th ) )
2	1	com12 32	. . 3 |- ( ( ps /\ ch ) -> ( ph -> th ) )
3	2	ex 450	. 2 |- ( ps -> ( ch -> ( ph -> th ) ) )
4	3	com3r 87	1 |- ( ph -> ( ps -> ( ch -> th ) ) )

Syntax hints:   -> wi 4   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  expdimp  453  expcomd  454  expdcom  455  pm3.3  460  syland  498  exp32  631  exp4b  632  exp4c  636  exp4d  637  exp42  639  exp44  641  exp5c  644  exp5j  645  exp5l  646  impl  650  mpan2d  710  a2and  853  3impib  1262  exp5o  1286  ax7  1943  ralrimivv  2970  mob2  3386  reuind  3411  reupick3  3912  elpwunsn  4224  disjiun  4640  sotr2  5064  wefrc  5108  relop  5272  predpoirr  5708  predfrirr  5709  suctrOLD  5809  fnun  5997  mpteqb  6299  funopsn  6413  tpres  6466  fconst5  6471  funfvima  6492  riotaeqimp  6634  dfwe2  6981  limuni3  7052  tfisi  7058  ordom  7074  funcnvuni  7119  f1oweALT  7152  frxp  7287  poxp  7289  wfr3g  7413  wfrlem12  7426  onfununi  7438  tz7.48lem  7536  oecl  7617  oaordex  7638  oaass  7641  omwordri  7652  odi  7659  omass  7660  omeu  7665  oen0  7666  oewordi  7671  oewordri  7672  nnarcl  7696  nnmass  7704  dif1en  8193  findcard2  8200  unblem1  8212  unblem2  8213  domunfican  8233  marypha1lem  8339  supiso  8381  inf3lem3  8527  epfrs  8607  karden  8758  infxpenlem  8836  iunfictbso  8937  dfac5  8951  dfac2  8953  kmlem1  8972  kmlem9  8980  infpssrlem3  9127  fin23lem25  9146  fin23lem30  9164  domtriomlem  9264  axdc3lem4  9275  axcclem  9279  zorn2lem7  9324  konigthlem  9390  wunr1om  9541  tskr1om  9589  gruen  9634  grur1a  9641  indpi  9729  genpnmax  9829  prlem934  9855  ltaddpr  9856  ltexprlem7  9864  ltaprlem  9866  axrrecex  9984  axpre-sup  9990  lelttr  10128  dedekind  10200  addid2  10219  nn0lt2  11440  fzind  11475  fnn0ind  11476  btwnz  11479  uzwo  11751  lbzbi  11776  rpnnen1lem5  11818  rpnnen1lem5OLD  11824  ledivge1le  11901  xrlelttr  11987  qbtwnre  12030  xrsupsslem  12137  xrinfmsslem  12138  supxrun  12146  elfz1b  12409  elfz0ubfz0  12443  elfzo0z  12509  fzofzim  12514  elfznelfzo  12573  fleqceilz  12653  fsequb  12774  leexp2r  12918  bernneq  12990  fi1uzind  13279  brfi1indALT  13282  fi1uzindOLD  13285  brfi1indALTOLD  13288  swrdnd2  13433  swrdswrdlem  13459  swrdswrd  13460  wrd2ind  13477  swrdccatin1  13483  swrdccatin2  13487  swrdccatin12lem3  13490  repswswrd  13531  cshweqrep  13567  swrd2lsw  13695  2swrd2eqwrdeq  13696  wrdl3s3  13705  s3iunsndisj  13707  cau3lem  14094  climuni  14283  mulcn2  14326  dvdsabseq  15035  divalglem8  15123  ndvdssub  15133  rplpwr  15276  algcvgblem  15290  lcmf  15346  lcmftp  15349  lcmfunsnlem2lem1  15351  lcmfunsnlem2lem2  15352  lcmfdvdsb  15356  lcmfun  15358  euclemma  15425  prmlem1a  15813  setsstruct2  15896  iscatd  16334  initoeu1  16661  initoeu2  16666  termoeu1  16668  plelttr  16972  grpinveu  17456  symgfixelsi  17855  efgred  18161  telgsumfzs  18386  srgmulgass  18531  srgbinom  18545  lspdisjb  19126  mplcoe5lem  19467  cply1mul  19664  coe1fzgsumd  19672  gsummoncoe1  19674  evl1gsumd  19721  cpmatacl  20521  cpmatmcllem  20523  basis2  20755  0ntr  20875  uncmp  21206  1stcrest  21256  txcls  21407  txcnp  21423  tx1stc  21453  fgss2  21678  alexsubALTlem2  21852  alexsubALTlem3  21853  alexsubALTlem4  21854  metcnp3  22345  tngngp3  22460  reconn  22631  iscau4  23077  ellimc3  23643  ulmbdd  24152  ulmcn  24153  sinq12ge0  24260  logblog  24530  gausslemma2dlem3  25093  ax5seglem5  25813  ax5seg  25818  uhgrnbgr0nb  26250  cplgrop  26333  wlkl1loop  26534  uspgr2wlkeq  26542  wlkres  26567  upgrwlkdvdelem  26632  uhgrwkspthlem2  26650  pthdlem2lem  26663  uspgrn2crct  26700  wlkiswwlks2lem3  26757  wlkiswwlks2  26761  wlkiswwlksupgr2  26763  wlklnwwlkln2lem  26768  wwlksnext  26788  wwlksnextfun  26793  rusgrnumwwlk  26870  clwlkclwwlklem2a4  26898  clwlkclwwlklem3  26902  erclwwlkssym  26935  erclwwlksnsym  26947  eleclclwwlksn  26953  upgr3v3e3cycl  27040  upgr4cycl4dv4e  27045  conngrv2edg  27055  eupth2lem3lem6  27093  frgrncvvdeqlem8  27170  frgrwopreglem4a  27174  numclwlk1lem2f1  27227  frgrreggt1  27251  frgrreg  27252  grpoinveu  27373  ococss  28152  shmodsi  28248  h1datomi  28440  hoaddsub  28675  adjmul  28951  chjatom  29216  atomli  29241  atcvat4i  29256  mdsymlem3  29264  mdsymlem5  29266  mdsymlem6  29267  sumdmdlem  29277  cdj3lem2a  29295  cdj3lem3a  29298  bnj1204  31080  cvmsdisj  31252  fundmpss  31664  dfon2lem6  31693  dfon2lem8  31695  frr3g  31779  frrlem11  31792  ifscgr  32151  lineext  32183  fscgr  32187  idinside  32191  btwnconn1lem11  32204  btwnconn1lem12  32205  btwnconn3  32210  brsegle  32215  seglecgr12  32218  hilbert1.2  32262  exp5d  32296  exp5k  32298  nn0prpwlem  32317  bj-restb  33047  poimirlem26  33435  poimirlem29  33438  poimirlem32  33441  areacirc  33505  heibor1lem  33608  pridl  33836  pridlc  33870  dmnnzd  33874  prtlem11  34151  prtlem17  34161  ax12indn  34228  atcvrj0  34714  cvrat4  34729  athgt  34742  lplnexllnN  34850  2llnjN  34853  lvolnle3at  34868  lncmp  35069  paddclN  35128  pexmidlem4N  35259  cdleme17d3  35784  cdleme50trn2  35839  cdlemf2  35850  cdlemf  35851  cdlemj3  36111  cdlemk26b-3  36193  dihord5b  36548  isnacs3  37273  jm2.26  37569  sbiota1  38635  exbir  38684  tratrb  38746  onfrALT  38764  in2an  38833  pwtrrVD  39060  suctrALT2VD  39071  suctrALT2  39072  tratrbVD  39097  trintALTVD  39116  trintALT  39117  zm1nn  41316  2ffzoeq  41338  iccpartiltu  41358  iccpartigtl  41359  iccpartgt  41363  iccpartnel  41374  fmtnofac2lem  41480  fmtnofac2  41481  lighneallem2  41523  odd2prm2  41627  stgoldbwt  41664  sbgoldbst  41666  sbgoldbaltlem1  41667  mogoldbb  41673  lidldomn1  41921  ply1mulgsumlem1  42174  lincsumcl  42220  ellcoellss  42224  islinindfis  42238  lindslinindsimp1  42246  lindslinindsimp2lem5  42251  lindsrng01  42257  elfzolborelfzop1  42309  aacllem  42547