MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  expd Structured version   Unicode version

Theorem expd 434
Description: Exportation deduction. (Contributed by NM, 20-Aug-1993.)
Hypothesis
Ref Expression
exp3a.1  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Assertion
Ref Expression
expd  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )

Proof of Theorem expd
StepHypRef Expression
1 exp3a.1 . . . 4  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
21com12 31 . . 3  |-  ( ( ps  /\  ch )  ->  ( ph  ->  th )
)
32ex 432 . 2  |-  ( ps 
->  ( ch  ->  ( ph  ->  th ) ) )
43com3r 79 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Colors of variables: wff setvar class
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:  expdimp  435  expcomd  436  expdcom  437  pm3.3  442  syland  479  exp32  603  exp4c  606  exp4d  607  exp42  609  exp44  611  exp5c  614  impl  618  mpan2d  672  a2and  809  3impib  1192  exp5o  1213  ax12indn  2275  mopickOLD  2354  ralrimivv  2874  mob2  3276  reuind  3300  reupick3  3780  elpwunsn  4057  disjiun  4430  sotr2  4818  wefrc  4862  suctr  4950  relop  5142  fnun  5669  mpteqb  5946  tpres  6100  fconst5  6105  funfvima  6122  dfwe2  6590  limuni3  6660  tfisi  6666  ordom  6682  funcnvuni  6726  f1oweALT  6757  frxp  6883  poxp  6885  onfununi  7004  tz7.48lem  7098  oecl  7179  oaordex  7199  oaass  7202  omwordri  7213  odi  7220  omass  7221  omeu  7226  oen0  7227  oewordi  7232  oewordri  7233  nnarcl  7257  nnmass  7265  dif1en  7745  findcard2  7752  unblem1  7764  unblem2  7765  domunfican  7785  marypha1lem  7885  supiso  7925  inf3lem3  8038  epfrs  8153  karden  8304  infxpenlem  8382  iunfictbso  8486  dfac5  8500  dfac2  8502  kmlem1  8521  kmlem9  8529  infpssrlem3  8676  fin23lem25  8695  fin23lem30  8713  domtriomlem  8813  axdc3lem4  8824  axcclem  8828  zorn2lem7  8873  konigthlem  8934  wunr1om  9086  tskr1om  9134  gruen  9179  grur1a  9186  indpi  9274  genpnmax  9374  prlem934  9400  ltaddpr  9401  ltexprlem7  9409  ltaprlem  9411  axrrecex  9529  axpre-sup  9535  lelttr  9664  dedekind  9733  addid2  9752  nn0lt2  10923  fzind  10958  fnn0ind  10959  btwnz  10962  uzwo  11145  uzwoOLD  11146  lbzbi  11171  rpnnen1lem5  11213  xrlelttr  11362  qbtwnre  11401  xrsupsslem  11501  xrinfmsslem  11502  supxrun  11510  elfz0ubfz0  11782  elfzo0z  11842  fzofzim  11846  elfznelfzo  11896  fleqceilz  11963  fsequb  12067  leexp2r  12205  bernneq  12274  brfi1uzind  12516  swrdnd2  12649  swrdswrdlem  12675  swrdswrd  12676  wrd2ind  12694  swrdccatin1  12699  swrdccatin2  12703  swrdccatin12lem3  12706  repswswrd  12747  cshweqrep  12780  swrd2lsw  12881  2swrd2eqwrdeq  12882  cau3lem  13269  climuni  13457  mulcn2  13500  divalglem8  14142  ndvdssub  14149  rplpwr  14278  algcvgblem  14290  euclemma  14333  prmlem1a  14676  iscatd  15162  initoeu1  15489  initoeu2  15494  termoeu1  15496  plelttr  15801  mndclOLD  16130  grpinveu  16283  symgfixelsi  16659  efgred  16965  telgsumfzs  17213  srgmulgass  17377  srgbinom  17391  lspdisjb  17967  mplcoe5lem  18325  cply1mul  18530  coe1fzgsumd  18539  gsummoncoe1  18541  evl1gsumd  18588  cpmatacl  19384  cpmatmcllem  19386  basis2  19619  0ntr  19739  uncmp  20070  1stcrest  20120  txcls  20271  txcnp  20287  tx1stc  20317  fgss2  20541  alexsubALTlem2  20714  alexsubALTlem3  20715  alexsubALTlem4  20716  metcnp3  21209  reconn  21499  iscau4  21884  ellimc3  22449  ulmbdd  22959  ulmcn  22960  sinq12ge0  23067  logblog  23331  ax5seglem5  24438  ax5seg  24443  wlkiswwlk2lem3  24895  wlkiswwlk2  24899  wlklniswwlkn2  24902  usg2wlkeq  24910  wwlknred  24925  wwlknext  24926  wwlkextfun  24931  clwlkisclwwlklem2a4  24986  clwlkisclwwlklem0  24990  wwlksubclwwlk  25006  erclwwlksym  25016  erclwwlknsym  25028  eleclclwwlkn  25035  cusgraisrusgra  25140  rusgranumwlk  25159  eupai  25169  frgrancvvdeqlemB  25240  frgrawopreglem5  25250  frg2woteq  25262  extwwlkfablem2  25280  numclwwlkovf2ex  25288  numclwlk1lem2f1  25296  frgrareggt1  25318  frgrareg  25319  grpoinveu  25422  gxneg  25466  gxsuc  25472  gxnn0add  25474  gxadd  25475  gxnn0mul  25477  gxmul  25478  ococss  26409  shmodsi  26505  h1datomi  26697  hoaddsub  26933  adjmul  27209  chjatom  27474  atomli  27499  atcvat4i  27514  mdsymlem3  27522  mdsymlem5  27524  mdsymlem6  27525  sumdmdlem  27535  cdj3lem2a  27553  cdj3lem3a  27556  cvmsdisj  28979  fundmpss  29437  dfon2lem6  29460  dfon2lem8  29462  predpoirr  29517  predfrirr  29518  wfr3g  29582  wfrlem12  29594  frr3g  29626  frrlem11  29639  ifscgr  29922  lineext  29954  fscgr  29958  idinside  29962  btwnconn1lem11  29975  btwnconn1lem12  29976  btwnconn3  29981  brsegle  29986  seglecgr12  29989  hilbert1.2  30033  areacirc  30352  exp5d  30358  exp5j  30360  exp5k  30361  exp5l  30362  nn0prpwlem  30380  heibor1lem  30545  pridl  30674  pridlc  30708  dmnnzd  30712  prtlem11  30847  prtlem17  30857  isnacs3  30882  jm2.26  31183  sbiota1  31582  zm1nn  32699  2ffzoeq  32715  lidldomn1  32981  ply1mulgsumlem1  33240  lincsumcl  33286  ellcoellss  33290  islinindfis  33304  lindslinindsimp1  33312  lindslinindsimp2lem5  33317  lindsrng01  33323  elfzolborelfzop1  33379  aacllem  33604  exbir  33606  tratrb  33697  onfrALT  33715  in2an  33788  pwtrrVD  34025  suctrALT2VD  34036  suctrALT2  34037  tratrbVD  34062  trintALTVD  34081  trintALT  34082  bnj1204  34469  atcvrj0  35549  cvrat4  35564  athgt  35577  lplnexllnN  35685  2llnjN  35688  lvolnle3at  35703  lncmp  35904  paddclN  35963  pexmidlem4N  36094  cdleme17d3  36619  cdleme50trn2  36674  cdlemf2  36685  cdlemf  36686  cdlemj3  36946  cdlemk26b-3  37028  dihord5b  37383
  Copyright terms: Public domain W3C validator