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

Theorem expd 438
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
StepHypRef Expression
1 expd.1 . . . 4  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
21com12 32 . . 3  |-  ( ( ps  /\  ch )  ->  ( ph  ->  th )
)
32ex 436 . 2  |-  ( ps 
->  ( ch  ->  ( ph  ->  th ) ) )
43com3r 82 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371
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 189  df-an 373
This theorem is referenced by:  expdimp  439  expcomd  440  expdcom  441  pm3.3  446  syland  484  exp32  610  exp4c  613  exp4d  614  exp42  616  exp44  618  exp5c  621  exp5j  622  impl  626  mpan2d  680  a2and  820  3impib  1206  exp5o  1228  ax7  1860  ralrimivv  2808  mob2  3218  reuind  3243  reupick3  3728  elpwunsn  4012  disjiun  4393  sotr2  4784  wefrc  4828  relop  4985  predpoirr  5408  predfrirr  5409  suctr  5506  fnun  5682  mpteqb  5964  tpres  6117  fconst5  6122  funfvima  6140  dfwe2  6608  limuni3  6679  tfisi  6685  ordom  6701  funcnvuni  6746  f1oweALT  6777  frxp  6906  poxp  6908  wfr3g  7034  wfrlem12  7047  onfununi  7060  tz7.48lem  7158  oecl  7239  oaordex  7259  oaass  7262  omwordri  7273  odi  7280  omass  7281  omeu  7286  oen0  7287  oewordi  7292  oewordri  7293  nnarcl  7317  nnmass  7325  dif1en  7804  findcard2  7811  unblem1  7823  unblem2  7824  domunfican  7844  marypha1lem  7947  supiso  7991  inf3lem3  8135  epfrs  8215  karden  8366  infxpenlem  8444  iunfictbso  8545  dfac5  8559  dfac2  8561  kmlem1  8580  kmlem9  8588  infpssrlem3  8735  fin23lem25  8754  fin23lem30  8772  domtriomlem  8872  axdc3lem4  8883  axcclem  8887  zorn2lem7  8932  konigthlem  8993  wunr1om  9144  tskr1om  9192  gruen  9237  grur1a  9244  indpi  9332  genpnmax  9432  prlem934  9458  ltaddpr  9459  ltexprlem7  9467  ltaprlem  9469  axrrecex  9587  axpre-sup  9593  lelttr  9724  dedekind  9797  addid2  9816  nn0lt2  11000  fzind  11033  fnn0ind  11034  btwnz  11037  uzwo  11222  lbzbi  11252  rpnnen1lem5  11294  xrlelttr  11453  qbtwnre  11492  xrsupsslem  11592  xrinfmsslem  11593  supxrun  11601  elfz0ubfz0  11894  elfzo0z  11958  fzofzim  11962  elfznelfzo  12014  fleqceilz  12081  fsequb  12188  leexp2r  12330  bernneq  12398  fi1uzind  12650  brfi1indALT  12653  swrdnd2  12789  swrdswrdlem  12815  swrdswrd  12816  wrd2ind  12834  swrdccatin1  12839  swrdccatin2  12843  swrdccatin12lem3  12846  repswswrd  12887  cshweqrep  12920  swrd2lsw  13027  2swrd2eqwrdeq  13028  cau3lem  13417  climuni  13616  mulcn2  13659  divalglem8  14380  ndvdssub  14388  rplpwr  14524  algcvgblem  14536  lcmf  14606  lcmftp  14609  lcmfunsnlem2lem1  14611  lcmfunsnlem2lem2  14612  lcmfdvdsb  14616  lcmfun  14618  euclemma  14665  prmlem1a  15078  iscatd  15579  initoeu1  15906  initoeu2  15911  termoeu1  15913  plelttr  16218  mndclOLD  16547  grpinveu  16700  symgfixelsi  17076  efgred  17398  telgsumfzs  17619  srgmulgass  17764  srgbinom  17778  lspdisjb  18349  mplcoe5lem  18691  cply1mul  18887  coe1fzgsumd  18896  gsummoncoe1  18898  evl1gsumd  18945  cpmatacl  19740  cpmatmcllem  19742  basis2  19966  0ntr  20087  uncmp  20418  1stcrest  20468  txcls  20619  txcnp  20635  tx1stc  20665  fgss2  20889  alexsubALTlem2  21063  alexsubALTlem3  21064  alexsubALTlem4  21065  metcnp3  21555  reconn  21846  iscau4  22249  ellimc3  22834  ulmbdd  23353  ulmcn  23354  sinq12ge0  23463  logblog  23729  ax5seglem5  24963  ax5seg  24968  wlkiswwlk2lem3  25421  wlkiswwlk2  25425  wlklniswwlkn2  25428  usg2wlkeq  25436  wwlknred  25451  wwlknext  25452  wwlkextfun  25457  clwlkisclwwlklem2a4  25512  clwlkisclwwlklem0  25516  wwlksubclwwlk  25532  erclwwlksym  25542  erclwwlknsym  25554  eleclclwwlkn  25561  cusgraisrusgra  25666  rusgranumwlk  25685  eupai  25695  frgrancvvdeqlemB  25766  frgrawopreglem5  25776  frg2woteq  25788  extwwlkfablem2  25806  numclwwlkovf2ex  25814  numclwlk1lem2f1  25822  frgrareggt1  25844  frgrareg  25845  grpoinveu  25950  gxneg  25994  gxsuc  26000  gxnn0add  26002  gxadd  26003  gxnn0mul  26005  gxmul  26006  ococss  26946  shmodsi  27042  h1datomi  27234  hoaddsub  27469  adjmul  27745  chjatom  28010  atomli  28035  atcvat4i  28050  mdsymlem3  28058  mdsymlem5  28060  mdsymlem6  28061  sumdmdlem  28071  cdj3lem2a  28089  cdj3lem3a  28092  bnj1204  29821  cvmsdisj  29993  fundmpss  30407  dfon2lem6  30434  dfon2lem8  30436  frr3g  30513  frrlem11  30526  ifscgr  30811  lineext  30843  fscgr  30847  idinside  30851  btwnconn1lem11  30864  btwnconn1lem12  30865  btwnconn3  30870  brsegle  30875  seglecgr12  30878  hilbert1.2  30922  exp5d  30957  exp5k  30959  exp5l  30960  nn0prpwlem  30978  poimirlem26  31966  poimirlem29  31969  poimirlem32  31972  areacirc  32037  heibor1lem  32141  pridl  32270  pridlc  32304  dmnnzd  32308  prtlem11  32438  prtlem17  32448  ax12indn  32514  atcvrj0  32993  cvrat4  33008  athgt  33021  lplnexllnN  33129  2llnjN  33132  lvolnle3at  33147  lncmp  33348  paddclN  33407  pexmidlem4N  33538  cdleme17d3  34063  cdleme50trn2  34118  cdlemf2  34129  cdlemf  34130  cdlemj3  34390  cdlemk26b-3  34472  dihord5b  34827  isnacs3  35552  jm2.26  35857  sbiota1  36785  exbir  36833  tratrb  36897  onfrALT  36915  in2an  36987  pwtrrVD  37221  suctrALT2VD  37232  suctrALT2  37233  tratrbVD  37258  trintALTVD  37277  trintALT  37278  iccpartiltu  38736  iccpartigtl  38737  iccpartgt  38741  iccpartnel  38752  stgoldbwt  38877  bgoldbst  38879  sgoldbaltlem1  38880  funopsn  39018  riotaeqimp  39037  zm1nn  39049  2ffzoeq  39064  uhgrnbgr0nb  39422  cplgrop  39504  upgrspths1wlklem  39696  lidldomn1  39974  ply1mulgsumlem1  40231  lincsumcl  40277  ellcoellss  40281  islinindfis  40295  lindslinindsimp1  40303  lindslinindsimp2lem5  40308  lindsrng01  40314  elfzolborelfzop1  40369  aacllem  40593
  Copyright terms: Public domain W3C validator