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  3impib  1185  exp5o  1206  ax12indn  2244  moOLD  2305  mopickOLD  2340  mopickOLDOLD  2341  ralrimivv  2828  mob2  3160  reuind  3183  reupick3  3656  elpwunsn  3938  disjiun  4303  sotr2  4691  wefrc  4735  suctr  4823  relop  5011  fnun  5538  mpteqb  5809  fconst5  5956  funfvima  5973  dfwe2  6414  limuni3  6484  tfisi  6490  ordom  6506  funcnvuni  6551  f1oweALT  6582  frxp  6703  poxp  6705  onfununi  6823  tz7.48lem  6917  oecl  6998  oaordex  7018  oaass  7021  omwordri  7032  odi  7039  omass  7040  omeu  7045  oen0  7046  oewordi  7051  oewordri  7052  nnarcl  7076  nnmass  7084  dif1enOLD  7565  dif1en  7566  findcard2  7573  unblem1  7585  unblem2  7586  domunfican  7605  marypha1lem  7704  supiso  7743  inf3lem3  7857  epfrs  7972  karden  8123  infxpenlem  8201  iunfictbso  8305  dfac5  8319  dfac2  8321  kmlem1  8340  kmlem9  8348  infpssrlem3  8495  fin23lem25  8514  fin23lem30  8532  domtriomlem  8632  axdc3lem4  8643  axcclem  8647  zorn2lem7  8692  konigthlem  8753  wunr1om  8907  tskr1om  8955  gruen  9000  grur1a  9007  indpi  9097  genpnmax  9197  prlem934  9223  ltaddpr  9224  ltexprlem7  9232  ltaprlem  9234  axrrecex  9351  axpre-sup  9357  lelttr  9486  dedekind  9554  addid2  9573  fzind  10761  fnn0ind  10762  btwnz  10765  uzwo  10938  uzwoOLD  10939  lbzbi  10964  rpnnen1lem5  11004  xrlelttr  11151  qbtwnre  11190  xrsupsslem  11290  xrinfmsslem  11291  supxrun  11299  elfzelfzelfz  11505  elfzo0z  11610  fzofzim  11614  ssfzo12bi  11643  elfznelfzo  11651  fleqceilz  11714  fsequb  11818  leexp2r  11942  bernneq  12011  brfi1uzind  12240  swrdvalodm2  12354  swrdvalodm  12355  swrdswrdlem  12374  swrdswrd  12375  wrd2ind  12393  swrdccatin1  12395  swrdccatin2  12399  swrdccatin12lem3  12402  swrdccat  12405  repswswrd  12443  cshweqrep  12476  swrd2lsw  12573  2swrd2eqwrdeq  12574  cau3lem  12863  climuni  13051  mulcn2  13094  divalglem8  13625  ndvdssub  13632  rplpwr  13761  algcvgblem  13773  euclemma  13815  prmlem1a  14155  iscatd  14632  plelttr  15163  grpinveu  15593  symgfixelsi  15961  efgred  16266  srgmulgass  16652  srgbinom  16665  lspdisjb  17229  mplcoe5lem  17569  evl1gsumd  17813  basis2  18578  0ntr  18697  uncmp  19028  1stcrest  19079  txcls  19199  txcnp  19215  tx1stc  19245  fgss2  19469  alexsubALTlem2  19642  alexsubALTlem3  19643  alexsubALTlem4  19644  metcnp3  20137  reconn  20427  iscau4  20812  ellimc3  21376  ulmbdd  21885  ulmcn  21886  sinq12ge0  21992  ax5seglem5  23201  ax5seg  23206  eupai  23610  grpoinveu  23731  gxneg  23775  gxsuc  23781  gxnn0add  23783  gxadd  23784  gxnn0mul  23786  gxmul  23787  ococss  24718  shmodsi  24814  h1datomi  25006  hoaddsub  25242  adjmul  25518  chjatom  25783  atomli  25808  atcvat4i  25823  mdsymlem3  25831  mdsymlem5  25833  mdsymlem6  25834  sumdmdlem  25844  cdj3lem2a  25862  cdj3lem3a  25865  cvmsdisj  27181  fundmpss  27599  dfon2lem6  27623  dfon2lem8  27625  predpoirr  27680  predfrirr  27681  wfr3g  27745  wfrlem12  27757  frr3g  27789  frrlem11  27802  ifscgr  28097  lineext  28129  fscgr  28133  idinside  28137  btwnconn1lem11  28150  btwnconn1lem12  28151  btwnconn3  28156  brsegle  28161  seglecgr12  28164  hilbert1.2  28208  areacirc  28515  exp5d  28521  exp5j  28523  exp5k  28524  exp5l  28525  nn0prpwlem  28543  heibor1lem  28734  pridl  28863  pridlc  28897  dmnnzd  28901  prtlem11  29037  prtlem17  29047  isnacs3  29072  jm2.26  29377  sbiota1  29714  nn0lt2  30212  2ffzoeq  30240  ccats1rev  30286  usg2wlkeq  30315  wlkiswwlk2lem3  30353  wlkiswwlk2  30357  wlklniswwlkn2  30360  wwlknred  30381  wwlknext  30382  wwlkextfun  30387  clwlkisclwwlklem2a4  30472  clwlkisclwwlklem0  30476  wwlksubclwwlk  30492  zm1nn  30494  erclwwlksym  30510  erclwwlknsym  30526  eleclclwwlkn  30533  cusgraisrusgra  30577  rusgranumwlk  30601  frgrancvvdeqlemB  30657  frgrawopreglem5  30667  frg2woteq  30679  extwwlkfablem2  30697  numclwwlkovf2ex  30705  numclwlk1lem2f1  30713  frgrareggt1  30735  frgrareg  30736  telescfzgsum  30843  coe1fzgsumd  30871  gsummoncoe1  30876  ply1mulgsumlem1  30877  cply1mul  30884  scmatsubcl  30923  scmatmulcl  30925  lincsumcl  30962  ellcoellss  30966  islinindfis  30980  lindslinindsimp1  30988  lindslinindsimp2lem5  30993  lindsrng01  30999  cnstpmatacl  31068  cnstpmatmcllem  31070  exbir  31250  tratrb  31338  onfrALT  31353  in2an  31426  pwtrrVD  31657  suctrALT2VD  31668  suctrALT2  31669  tratrbVD  31693  trintALTVD  31712  trintALT  31713  bnj1204  32099  atcvrj0  33168  cvrat4  33183  athgt  33196  lplnexllnN  33304  2llnjN  33307  lvolnle3at  33322  lncmp  33523  paddclN  33582  pexmidlem4N  33713  cdleme17d3  34236  cdleme50trn2  34291  cdlemf2  34302  cdlemf  34303  cdlemj3  34563  cdlemk26b-3  34645  dihord5b  35000
  Copyright terms: Public domain W3C validator