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

Theorem expd 436
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 434 . 2  |-  ( ps 
->  ( ch  ->  ( ph  ->  th ) ) )
43com3r 79 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Colors of variables: wff setvar class
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:  expdimp  437  expcomd  438  expdcom  439  pm3.3  444  syland  481  exp32  605  exp4c  608  exp4d  609  exp42  611  exp44  613  exp5c  616  impl  620  mpan2d  674  a2and  809  3impib  1193  exp5o  1214  ax12indn  2257  mopickOLD  2341  ralrimivv  2861  mob2  3263  reuind  3287  reupick3  3766  elpwunsn  4052  disjiun  4424  sotr2  4816  wefrc  4860  suctr  4948  relop  5140  fnun  5674  mpteqb  5952  fconst5  6110  funfvima  6129  dfwe2  6599  limuni3  6669  tfisi  6675  ordom  6691  funcnvuni  6735  f1oweALT  6766  frxp  6892  poxp  6894  onfununi  7011  tz7.48lem  7105  oecl  7186  oaordex  7206  oaass  7209  omwordri  7220  odi  7227  omass  7228  omeu  7233  oen0  7234  oewordi  7239  oewordri  7240  nnarcl  7264  nnmass  7272  dif1enOLD  7751  dif1en  7752  findcard2  7759  unblem1  7771  unblem2  7772  domunfican  7792  marypha1lem  7892  supiso  7933  inf3lem3  8047  epfrs  8162  karden  8313  infxpenlem  8391  iunfictbso  8495  dfac5  8509  dfac2  8511  kmlem1  8530  kmlem9  8538  infpssrlem3  8685  fin23lem25  8704  fin23lem30  8722  domtriomlem  8822  axdc3lem4  8833  axcclem  8837  zorn2lem7  8882  konigthlem  8943  wunr1om  9097  tskr1om  9145  gruen  9190  grur1a  9197  indpi  9285  genpnmax  9385  prlem934  9411  ltaddpr  9412  ltexprlem7  9420  ltaprlem  9422  axrrecex  9540  axpre-sup  9546  lelttr  9675  dedekind  9744  addid2  9763  nn0lt2  10930  fzind  10964  fnn0ind  10965  btwnz  10968  uzwo  11150  uzwoOLD  11151  lbzbi  11176  rpnnen1lem5  11218  xrlelttr  11365  qbtwnre  11404  xrsupsslem  11504  xrinfmsslem  11505  supxrun  11513  elfz0ubfz0  11783  elfzo0z  11841  fzofzim  11845  elfznelfzo  11891  fleqceilz  11957  fsequb  12061  leexp2r  12199  bernneq  12268  brfi1uzind  12508  swrdvalodm2  12640  swrdvalodm  12641  swrdswrdlem  12660  swrdswrd  12661  wrd2ind  12679  swrdccatin1  12684  swrdccatin2  12688  swrdccatin12lem3  12691  repswswrd  12732  cshweqrep  12765  swrd2lsw  12866  2swrd2eqwrdeq  12867  cau3lem  13163  climuni  13351  mulcn2  13394  divalglem8  13932  ndvdssub  13939  rplpwr  14068  algcvgblem  14080  euclemma  14123  prmlem1a  14466  iscatd  14944  plelttr  15473  mndclOLD  15802  grpinveu  15955  symgfixelsi  16331  efgred  16637  telgsumfzs  16889  srgmulgass  17053  srgbinom  17067  lspdisjb  17643  mplcoe5lem  18001  cply1mul  18206  coe1fzgsumd  18215  gsummoncoe1  18217  evl1gsumd  18264  cpmatacl  19087  cpmatmcllem  19089  basis2  19322  0ntr  19442  uncmp  19773  1stcrest  19824  txcls  19975  txcnp  19991  tx1stc  20021  fgss2  20245  alexsubALTlem2  20418  alexsubALTlem3  20419  alexsubALTlem4  20420  metcnp3  20913  reconn  21203  iscau4  21588  ellimc3  22153  ulmbdd  22662  ulmcn  22663  sinq12ge0  22770  ax5seglem5  24105  ax5seg  24110  wlkiswwlk2lem3  24562  wlkiswwlk2  24566  wlklniswwlkn2  24569  usg2wlkeq  24577  wwlknred  24592  wwlknext  24593  wwlkextfun  24598  clwlkisclwwlklem2a4  24653  clwlkisclwwlklem0  24657  wwlksubclwwlk  24673  erclwwlksym  24683  erclwwlknsym  24695  eleclclwwlkn  24702  cusgraisrusgra  24807  rusgranumwlk  24826  eupai  24836  frgrancvvdeqlemB  24907  frgrawopreglem5  24917  frg2woteq  24929  extwwlkfablem2  24947  numclwwlkovf2ex  24955  numclwlk1lem2f1  24963  frgrareggt1  24985  frgrareg  24986  grpoinveu  25093  gxneg  25137  gxsuc  25143  gxnn0add  25145  gxadd  25146  gxnn0mul  25148  gxmul  25149  ococss  26080  shmodsi  26176  h1datomi  26368  hoaddsub  26604  adjmul  26880  chjatom  27145  atomli  27170  atcvat4i  27185  mdsymlem3  27193  mdsymlem5  27195  mdsymlem6  27196  sumdmdlem  27206  cdj3lem2a  27224  cdj3lem3a  27227  cvmsdisj  28585  fundmpss  29168  dfon2lem6  29192  dfon2lem8  29194  predpoirr  29249  predfrirr  29250  wfr3g  29314  wfrlem12  29326  frr3g  29358  frrlem11  29371  ifscgr  29666  lineext  29698  fscgr  29702  idinside  29706  btwnconn1lem11  29719  btwnconn1lem12  29720  btwnconn3  29725  brsegle  29730  seglecgr12  29733  hilbert1.2  29777  areacirc  30084  exp5d  30090  exp5j  30092  exp5k  30093  exp5l  30094  nn0prpwlem  30112  heibor1lem  30277  pridl  30406  pridlc  30440  dmnnzd  30444  prtlem11  30579  prtlem17  30589  isnacs3  30614  jm2.26  30916  sbiota1  31292  zm1nn  32163  2ffzoeq  32179  tpres  32390  lidldomn1  32434  ply1mulgsumlem1  32716  lincsumcl  32762  ellcoellss  32766  islinindfis  32780  lindslinindsimp1  32788  lindslinindsimp2lem5  32793  lindsrng01  32799  exbir  32947  tratrb  33035  onfrALT  33049  in2an  33122  pwtrrVD  33353  suctrALT2VD  33364  suctrALT2  33365  tratrbVD  33389  trintALTVD  33408  trintALT  33409  bnj1204  33796  atcvrj0  34875  cvrat4  34890  athgt  34903  lplnexllnN  35011  2llnjN  35014  lvolnle3at  35029  lncmp  35230  paddclN  35289  pexmidlem4N  35420  cdleme17d3  35945  cdleme50trn2  36000  cdlemf2  36011  cdlemf  36012  cdlemj3  36272  cdlemk26b-3  36354  dihord5b  36709
  Copyright terms: Public domain W3C validator