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

Theorem exp3a 426
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 29 . . 3  |-  ( ( ps  /\  ch )  ->  ( ph  ->  th )
)
32ex 424 . 2  |-  ( ps 
->  ( ch  ->  ( ph  ->  th ) ) )
43com3r 75 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  expdimp  427  pm3.3  432  syland  468  exp32  589  exp4c  592  exp4d  593  exp42  595  exp44  597  exp5c  600  impl  604  mpan2d  656  3impib  1151  exp5o  1172  exbir  1371  exp3acom3r  1376  exp3acom23  1378  nfsb4t  2113  ax11indn  2229  mo  2260  mopick  2300  ralrimivv  2740  mob2  3057  reuind  3080  reupick3  3569  disjiun  4143  sotr2  4473  wefrc  4517  suctr  4605  elpwunsn  4697  dfwe2  4702  limuni3  4772  tfisi  4778  ordom  4794  relop  4963  funcnvuni  5458  fnun  5491  mpteqb  5758  fconst5  5888  funfvima  5912  f1oweALT  6013  frxp  6392  poxp  6394  riotasv3dOLD  6535  onfununi  6539  tfrlem5  6577  tz7.48lem  6634  oecl  6717  oaordex  6737  oaass  6740  omwordri  6751  odi  6758  omass  6759  omeu  6764  oen0  6765  oewordi  6770  oewordri  6771  nnarcl  6795  nnmass  6803  dif1enOLD  7276  dif1en  7277  findcard2  7284  unblem1  7295  unblem2  7296  domunfican  7315  marypha1lem  7373  supiso  7410  inf3lem3  7518  epfrs  7600  karden  7752  infxpenlem  7828  iunfictbso  7928  dfac5  7942  dfac2  7944  kmlem1  7963  kmlem9  7971  infpssrlem3  8118  fin23lem25  8137  fin23lem30  8155  domtriomlem  8255  axdc3lem4  8266  axcclem  8270  zorn2lem7  8315  konigthlem  8376  wunr1om  8527  tskr1om  8575  gruen  8620  grur1a  8627  indpi  8717  genpnmax  8817  prlem934  8843  ltaddpr  8844  ltexprlem7  8852  ltaprlem  8854  axrrecex  8971  axpre-sup  8977  lelttr  9098  addid2  9181  fzind  10300  fnn0ind  10301  btwnz  10304  uzwo  10471  uzwoOLD  10472  lbzbi  10496  rpnnen1lem5  10536  xrlelttr  10678  qbtwnre  10717  xrsupsslem  10817  xrinfmsslem  10818  supxrun  10826  elfznelfzo  11119  fsequb  11241  leexp2r  11364  bernneq  11432  brfi1uzind  11642  cau3lem  12085  climuni  12273  mulcn2  12316  divalglem8  12847  ndvdssub  12854  rplpwr  12983  algcvgblem  12995  euclemma  13035  prmlem1a  13356  iscatd  13825  plelttr  14356  grpinveu  14766  efgred  15307  lspdisjb  16125  basis2  16939  0ntr  17058  uncmp  17388  1stcrest  17437  txcls  17557  txcnp  17573  tx1stc  17603  fgss2  17827  alexsubALTlem2  18000  alexsubALTlem3  18001  alexsubALTlem4  18002  metcnp3  18460  reconn  18730  iscau4  19103  ellimc3  19633  ulmbdd  20181  ulmcn  20182  sinq12ge0  20283  eupai  21537  grpoinveu  21658  gxneg  21702  gxsuc  21708  gxnn0add  21710  gxadd  21711  gxnn0mul  21713  gxmul  21714  ococss  22643  shmodsi  22739  h1datomi  22931  hoaddsub  23167  adjmul  23443  chjatom  23708  atomli  23733  atcvat4i  23748  mdsymlem3  23756  mdsymlem5  23758  mdsymlem6  23759  sumdmdlem  23769  cdj3lem2a  23787  cdj3lem3a  23790  cvmsdisj  24736  dedekind  24966  fundmpss  25146  dfon2lem6  25168  dfon2lem8  25170  predpoirr  25221  predfrirr  25222  wfr3g  25279  wfrlem12  25291  frr3g  25304  frrlem11  25317  ax5seglem5  25586  ax5seg  25591  ifscgr  25692  lineext  25724  fscgr  25728  idinside  25732  btwnconn1lem11  25745  btwnconn1lem12  25746  btwnconn3  25751  brsegle  25756  seglecgr12  25759  hilbert1.2  25803  itg2addnc  25959  areacirc  25988  exp5d  25994  exp5j  25996  exp5k  25997  exp5l  25998  nn0prpwlem  26016  heibor1lem  26209  pridl  26338  pridlc  26372  dmnnzd  26376  prtlem11  26406  prtlem17  26416  isnacs3  26455  jm2.26  26764  sbiota1  27303  frgrancvvdeqlemB  27790  frgrawopreglem5  27800  tratrb  27963  onfrALT  27978  in2an  28050  pwtrrVD  28279  suctrALT2VD  28289  suctrALT2  28290  tratrbVD  28314  trintALTVD  28333  trintALT  28334  bnj1204  28719  nfsb4twAUX7  28912  nfsb4tOLD7  29061  nfsb4tw2AUXOLD7  29062  atcvrj0  29542  cvrat4  29557  athgt  29570  lplnexllnN  29678  2llnjN  29681  lvolnle3at  29696  lncmp  29897  paddclN  29956  pexmidlem4N  30087  cdleme17d3  30610  cdleme50trn2  30665  cdlemf2  30676  cdlemf  30677  cdlemj3  30937  cdlemk26b-3  31019  dihord5b  31374
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator