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  1194  exp5o  1215  ax12indn  2266  moOLD  2327  mopickOLD  2362  mopickOLDOLD  2363  ralrimivv  2884  mob2  3283  reuind  3307  reupick3  3783  elpwunsn  4068  disjiun  4437  sotr2  4829  wefrc  4873  suctr  4961  relop  5153  fnun  5687  mpteqb  5965  fconst5  6119  funfvima  6136  dfwe2  6602  limuni3  6672  tfisi  6678  ordom  6694  funcnvuni  6738  f1oweALT  6769  frxp  6894  poxp  6896  onfununi  7013  tz7.48lem  7107  oecl  7188  oaordex  7208  oaass  7211  omwordri  7222  odi  7229  omass  7230  omeu  7235  oen0  7236  oewordi  7241  oewordri  7242  nnarcl  7266  nnmass  7274  dif1enOLD  7753  dif1en  7754  findcard2  7761  unblem1  7773  unblem2  7774  domunfican  7794  marypha1lem  7894  supiso  7934  inf3lem3  8048  epfrs  8163  karden  8314  infxpenlem  8392  iunfictbso  8496  dfac5  8510  dfac2  8512  kmlem1  8531  kmlem9  8539  infpssrlem3  8686  fin23lem25  8705  fin23lem30  8723  domtriomlem  8823  axdc3lem4  8834  axcclem  8838  zorn2lem7  8883  konigthlem  8944  wunr1om  9098  tskr1om  9146  gruen  9191  grur1a  9198  indpi  9286  genpnmax  9386  prlem934  9412  ltaddpr  9413  ltexprlem7  9421  ltaprlem  9423  axrrecex  9541  axpre-sup  9547  lelttr  9676  dedekind  9744  addid2  9763  nn0lt2  10926  fzind  10960  fnn0ind  10961  btwnz  10964  uzwo  11145  uzwoOLD  11146  lbzbi  11171  rpnnen1lem5  11213  xrlelttr  11360  qbtwnre  11399  xrsupsslem  11499  xrinfmsslem  11500  supxrun  11508  elfz0ubfz0  11777  elfzo0z  11834  fzofzim  11838  ssfzo12bi  11876  elfznelfzo  11884  fleqceilz  11950  fsequb  12054  leexp2r  12192  bernneq  12261  brfi1uzind  12499  swrdvalodm2  12630  swrdvalodm  12631  swrdswrdlem  12650  swrdswrd  12651  wrd2ind  12669  swrdccatin1  12674  swrdccatin2  12678  swrdccatin12lem3  12681  swrdccat  12684  repswswrd  12722  cshweqrep  12755  swrd2lsw  12856  2swrd2eqwrdeq  12857  cau3lem  13153  climuni  13341  mulcn2  13384  divalglem8  13920  ndvdssub  13927  rplpwr  14056  algcvgblem  14068  euclemma  14111  prmlem1a  14453  iscatd  14931  plelttr  15462  grpinveu  15898  symgfixelsi  16274  efgred  16581  telgsumfzs  16833  srgmulgass  16996  srgbinom  17010  lspdisjb  17584  mplcoe5lem  17941  cply1mul  18146  coe1fzgsumd  18155  gsummoncoe1  18157  evl1gsumd  18204  cpmatacl  19024  cpmatmcllem  19026  basis2  19259  0ntr  19378  uncmp  19709  1stcrest  19760  txcls  19932  txcnp  19948  tx1stc  19978  fgss2  20202  alexsubALTlem2  20375  alexsubALTlem3  20376  alexsubALTlem4  20377  metcnp3  20870  reconn  21160  iscau4  21545  ellimc3  22110  ulmbdd  22619  ulmcn  22620  sinq12ge0  22726  ax5seglem5  24009  ax5seg  24014  wlkiswwlk2lem3  24466  wlkiswwlk2  24470  wlklniswwlkn2  24473  usg2wlkeq  24481  wwlknred  24496  wwlknext  24497  wwlkextfun  24502  clwlkisclwwlklem2a4  24557  clwlkisclwwlklem0  24561  wwlksubclwwlk  24577  erclwwlksym  24587  erclwwlknsym  24599  eleclclwwlkn  24606  cusgraisrusgra  24711  rusgranumwlk  24730  eupai  24740  frgrancvvdeqlemB  24812  frgrawopreglem5  24822  frg2woteq  24834  extwwlkfablem2  24852  numclwwlkovf2ex  24860  numclwlk1lem2f1  24868  frgrareggt1  24890  frgrareg  24891  grpoinveu  24997  gxneg  25041  gxsuc  25047  gxnn0add  25049  gxadd  25050  gxnn0mul  25052  gxmul  25053  ococss  25984  shmodsi  26080  h1datomi  26272  hoaddsub  26508  adjmul  26784  chjatom  27049  atomli  27074  atcvat4i  27089  mdsymlem3  27097  mdsymlem5  27099  mdsymlem6  27100  sumdmdlem  27110  cdj3lem2a  27128  cdj3lem3a  27131  cvmsdisj  28466  fundmpss  29049  dfon2lem6  29073  dfon2lem8  29075  predpoirr  29130  predfrirr  29131  wfr3g  29195  wfrlem12  29207  frr3g  29239  frrlem11  29252  ifscgr  29547  lineext  29579  fscgr  29583  idinside  29587  btwnconn1lem11  29600  btwnconn1lem12  29601  btwnconn3  29606  brsegle  29611  seglecgr12  29614  hilbert1.2  29658  areacirc  29965  exp5d  29971  exp5j  29973  exp5k  29974  exp5l  29975  nn0prpwlem  29993  heibor1lem  30135  pridl  30264  pridlc  30298  dmnnzd  30302  prtlem11  30438  prtlem17  30448  isnacs3  30473  jm2.26  30775  sbiota1  31146  zm1nn  32019  2ffzoeq  32035  ply1mulgsumlem1  32284  lincsumcl  32330  ellcoellss  32334  islinindfis  32348  lindslinindsimp1  32356  lindslinindsimp2lem5  32361  lindsrng01  32367  exbir  32515  tratrb  32603  onfrALT  32618  in2an  32691  pwtrrVD  32922  suctrALT2VD  32933  suctrALT2  32934  tratrbVD  32958  trintALTVD  32977  trintALT  32978  bnj1204  33364  atcvrj0  34441  cvrat4  34456  athgt  34469  lplnexllnN  34577  2llnjN  34580  lvolnle3at  34595  lncmp  34796  paddclN  34855  pexmidlem4N  34986  cdleme17d3  35509  cdleme50trn2  35564  cdlemf2  35575  cdlemf  35576  cdlemj3  35836  cdlemk26b-3  35918  dihord5b  36273
  Copyright terms: Public domain W3C validator