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

Theorem exp3a 425
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 27 . . 3  |-  ( ( ps  /\  ch )  ->  ( ph  ->  th )
)
32ex 423 . 2  |-  ( ps 
->  ( ch  ->  ( ph  ->  th ) ) )
43com3r 73 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  expdimp  426  pm3.3  431  syland  467  exp32  588  exp4c  591  exp4d  592  exp42  594  exp44  596  exp5c  599  impl  603  mpan2d  655  3impib  1149  exp5o  1170  exbir  1355  exp3acom3r  1360  exp3acom23  1362  nfsb4t  2022  ax11indn  2136  mo  2167  mopick  2207  ralrimivv  2636  mob2  2947  reuind  2970  reupick3  3455  disjiun  4015  sotr2  4345  wefrc  4389  suctr  4477  elpwunsn  4570  dfwe2  4575  limuni3  4645  tfisi  4651  ordom  4667  relop  4836  funcnvuni  5319  fnun  5352  mpteqb  5616  fconst5  5733  funfvima  5755  f1oweALT  5853  frxp  6227  poxp  6229  riotasv3dOLD  6356  onfununi  6360  tfrlem5  6398  tz7.48lem  6455  oecl  6538  oaordex  6558  oaass  6561  omwordri  6572  odi  6579  omass  6580  omeu  6585  oen0  6586  oewordi  6591  oewordri  6592  nnarcl  6616  nnmass  6624  dif1enOLD  7092  dif1en  7093  findcard2  7100  unblem1  7111  unblem2  7112  domunfican  7131  marypha1lem  7188  supiso  7225  inf3lem3  7333  epfrs  7415  karden  7567  infxpenlem  7643  iunfictbso  7743  dfac5  7757  dfac2  7759  kmlem1  7778  kmlem9  7786  infpssrlem3  7933  fin23lem25  7952  fin23lem30  7970  domtriomlem  8070  axdc3lem4  8081  axcclem  8085  zorn2lem7  8131  konigthlem  8192  wunr1om  8343  tskr1om  8391  gruen  8436  grur1a  8443  indpi  8533  genpnmax  8633  prlem934  8659  ltaddpr  8660  ltexprlem7  8668  ltaprlem  8670  axrrecex  8787  axpre-sup  8793  lelttr  8914  addid2  8997  fzind  10112  fnn0ind  10113  btwnz  10116  uzwo  10283  uzwoOLD  10284  lbzbi  10308  rpnnen1lem5  10348  xrlelttr  10489  qbtwnre  10528  xrsupsslem  10627  xrinfmsslem  10628  supxrun  10636  fsequb  11039  leexp2r  11161  bernneq  11229  cau3lem  11840  climuni  12028  mulcn2  12071  divalglem8  12601  ndvdssub  12608  rplpwr  12737  algcvgblem  12749  euclemma  12789  prmlem1a  13110  iscatd  13577  plelttr  14108  grpinveu  14518  efgred  15059  lspdisjb  15881  basis2  16691  0ntr  16810  uncmp  17132  1stcrest  17181  txcls  17301  txcnp  17316  tx1stc  17346  fgss2  17571  alexsubALTlem2  17744  alexsubALTlem3  17745  alexsubALTlem4  17746  metcnp3  18088  reconn  18335  iscau4  18707  ellimc3  19231  ulmbdd  19777  ulmcn  19778  sinq12ge0  19878  grpoinveu  20891  gxneg  20935  gxsuc  20941  gxnn0add  20943  gxadd  20944  gxnn0mul  20946  gxmul  20947  ococss  21874  shmodsi  21970  h1datomi  22162  hoaddsub  22398  adjmul  22674  chjatom  22939  atomli  22964  atcvat4i  22979  mdsymlem3  22987  mdsymlem5  22989  mdsymlem6  22990  sumdmdlem  23000  cdj3lem2a  23018  cdj3lem3a  23021  cvmsdisj  23803  eupai  23885  dedekind  24084  fundmpss  24124  dfon2lem6  24146  dfon2lem8  24148  predpoirr  24199  predfrirr  24200  wfr3g  24257  wfrlem12  24269  frr3g  24282  frrlem11  24295  ax5seglem5  24563  ax5seg  24568  ifscgr  24669  lineext  24701  fscgr  24705  idinside  24709  btwnconn1lem11  24722  btwnconn1lem12  24723  btwnconn3  24728  brsegle  24733  seglecgr12  24736  hilbert1.2  24780  itg2addnc  24935  areacirc  24942  elioo1t3  25513  iintlem1  25621  clscnc  26021  exp5d  26219  exp5j  26221  exp5k  26222  exp5l  26223  nn0prpwlem  26249  heibor1lem  26544  pridl  26673  pridlc  26707  dmnnzd  26711  prtlem11  26745  prtlem17  26755  isnacs3  26796  jm2.26  27106  sbiota1  27645  stoweidlem17  27777  stoweidlem62  27822  tratrb  28355  onfrALT  28370  in2an  28442  pwtrrVD  28673  pwtrrOLD  28674  suctrALT2VD  28685  suctrALT2  28686  tratrbVD  28710  trintALTVD  28729  trintALT  28730  bnj1204  29115  atcvrj0  29690  cvrat4  29705  athgt  29718  lplnexllnN  29826  2llnjN  29829  lvolnle3at  29844  lncmp  30045  paddclN  30104  pexmidlem4N  30235  cdleme17d3  30758  cdleme50trn2  30813  cdlemf2  30824  cdlemf  30825  cdlemj3  31085  cdlemk26b-3  31167  dihord5b  31522
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 177  df-an 360
  Copyright terms: Public domain W3C validator