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

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

Proof of Theorem exp3a
StepHypRef Expression
1 exp3a.1 . . . 4  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
21com12 30 . . 3  |-  ( ( ps  /\  ch )  ->  ( ph  ->  th )
)
32ex 425 . 2  |-  ( ps 
->  ( ch  ->  ( ph  ->  th ) ) )
43com3r 76 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  expdimp  428  pm3.3  433  syland  469  exp32  590  exp4c  593  exp4d  594  exp42  596  exp44  598  exp5c  601  impl  605  mpan2d  657  3impib  1152  exp5o  1173  exbir  1375  exp3acom3r  1380  exp3acom23  1382  nfsb4tOLD  2130  ax11indn  2274  mo  2305  mopick  2345  ralrimivv  2799  mob2  3116  reuind  3139  reupick3  3628  disjiun  4205  sotr2  4535  wefrc  4579  suctrALT  4667  elpwunsn  4760  dfwe2  4765  limuni3  4835  tfisi  4841  ordom  4857  relop  5026  funcnvuni  5521  fnun  5554  mpteqb  5822  fconst5  5952  funfvima  5976  f1oweALT  6077  frxp  6459  poxp  6461  riotasv3dOLD  6602  onfununi  6606  tfrlem5  6644  tz7.48lem  6701  oecl  6784  oaordex  6804  oaass  6807  omwordri  6818  odi  6825  omass  6826  omeu  6831  oen0  6832  oewordi  6837  oewordri  6838  nnarcl  6862  nnmass  6870  dif1enOLD  7343  dif1en  7344  findcard2  7351  unblem1  7362  unblem2  7363  domunfican  7382  marypha1lem  7441  supiso  7480  inf3lem3  7588  epfrs  7670  karden  7824  infxpenlem  7900  iunfictbso  8000  dfac5  8014  dfac2  8016  kmlem1  8035  kmlem9  8043  infpssrlem3  8190  fin23lem25  8209  fin23lem30  8227  domtriomlem  8327  axdc3lem4  8338  axcclem  8342  zorn2lem7  8387  konigthlem  8448  wunr1om  8599  tskr1om  8647  gruen  8692  grur1a  8699  indpi  8789  genpnmax  8889  prlem934  8915  ltaddpr  8916  ltexprlem7  8924  ltaprlem  8926  axrrecex  9043  axpre-sup  9049  lelttr  9170  addid2  9254  fzind  10373  fnn0ind  10374  btwnz  10377  uzwo  10544  uzwoOLD  10545  lbzbi  10569  rpnnen1lem5  10609  xrlelttr  10751  qbtwnre  10790  xrsupsslem  10890  xrinfmsslem  10891  supxrun  10899  elfznelfzo  11197  fsequb  11319  leexp2r  11442  bernneq  11510  brfi1uzind  11720  cau3lem  12163  climuni  12351  mulcn2  12394  divalglem8  12925  ndvdssub  12932  rplpwr  13061  algcvgblem  13073  euclemma  13113  prmlem1a  13434  iscatd  13903  plelttr  14434  grpinveu  14844  efgred  15385  lspdisjb  16203  basis2  17021  0ntr  17140  uncmp  17471  1stcrest  17521  txcls  17641  txcnp  17657  tx1stc  17687  fgss2  17911  alexsubALTlem2  18084  alexsubALTlem3  18085  alexsubALTlem4  18086  metcnp3  18575  reconn  18864  iscau4  19237  ellimc3  19771  ulmbdd  20319  ulmcn  20320  sinq12ge0  20421  eupai  21694  grpoinveu  21815  gxneg  21859  gxsuc  21865  gxnn0add  21867  gxadd  21868  gxnn0mul  21870  gxmul  21871  ococss  22800  shmodsi  22896  h1datomi  23088  hoaddsub  23324  adjmul  23600  chjatom  23865  atomli  23890  atcvat4i  23905  mdsymlem3  23913  mdsymlem5  23915  mdsymlem6  23916  sumdmdlem  23926  cdj3lem2a  23944  cdj3lem3a  23947  cvmsdisj  24962  dedekind  25192  fundmpss  25395  dfon2lem6  25420  dfon2lem8  25422  predpoirr  25477  predfrirr  25478  wfr3g  25542  wfrlem12  25554  frr3g  25586  frrlem11  25599  ax5seglem5  25877  ax5seg  25882  ifscgr  25983  lineext  26015  fscgr  26019  idinside  26023  btwnconn1lem11  26036  btwnconn1lem12  26037  btwnconn3  26042  brsegle  26047  seglecgr12  26050  hilbert1.2  26094  areacirc  26311  exp5d  26317  exp5j  26319  exp5k  26320  exp5l  26321  nn0prpwlem  26339  heibor1lem  26532  pridl  26661  pridlc  26695  dmnnzd  26699  prtlem11  26729  prtlem17  26739  isnacs3  26778  jm2.26  27087  sbiota1  27625  elfzelfzelfz  28132  fzofzim  28159  2ffzoeq  28163  swrdvalodm2  28222  swrdvalodm  28223  swrd0swrd  28231  swrdswrdlem  28232  swrdswrd  28233  swrdccatin1  28239  swrdccatin2  28244  swrdccatin12lem4  28247  swrdccat  28250  2cshw1lem2  28283  2cshwmod  28291  usg2wlkeq  28342  wlkiswwlk2lem3  28375  wlkiswwlk2  28379  wlklniswwlkn2  28382  cusgraisrusgra  28449  frgrancvvdeqlemB  28501  frgrawopreglem5  28511  frg2woteq  28523  tratrb  28694  onfrALT  28709  in2an  28783  pwtrrVD  29012  suctrALT2VD  29022  suctrALT2  29023  tratrbVD  29047  trintALTVD  29066  trintALT  29067  bnj1204  29455  nfsb4twAUX7  29650  nfsb4tOLD7  29819  nfsb4tw2AUXOLD7  29820  atcvrj0  30299  cvrat4  30314  athgt  30327  lplnexllnN  30435  2llnjN  30438  lvolnle3at  30453  lncmp  30654  paddclN  30713  pexmidlem4N  30844  cdleme17d3  31367  cdleme50trn2  31422  cdlemf2  31433  cdlemf  31434  cdlemj3  31694  cdlemk26b-3  31776  dihord5b  32131
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 179  df-an 362
  Copyright terms: Public domain W3C validator