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  2020  ax11indn  2134  mo  2165  mopick  2205  ralrimivv  2634  mob2  2945  reuind  2968  reupick3  3453  disjiun  4013  sotr2  4343  wefrc  4387  suctr  4475  elpwunsn  4568  dfwe2  4573  limuni3  4643  tfisi  4649  ordom  4665  relop  4834  funcnvuni  5317  fnun  5350  mpteqb  5614  fconst5  5731  funfvima  5753  f1oweALT  5851  frxp  6225  poxp  6227  riotasv3dOLD  6354  onfununi  6358  tfrlem5  6396  tz7.48lem  6453  oecl  6536  oaordex  6556  oaass  6559  omwordri  6570  odi  6577  omass  6578  omeu  6583  oen0  6584  oewordi  6589  oewordri  6590  nnarcl  6614  nnmass  6622  dif1enOLD  7090  dif1en  7091  findcard2  7098  unblem1  7109  unblem2  7110  domunfican  7129  marypha1lem  7186  supiso  7223  inf3lem3  7331  epfrs  7413  karden  7565  infxpenlem  7641  iunfictbso  7741  dfac5  7755  dfac2  7757  kmlem1  7776  kmlem9  7784  infpssrlem3  7931  fin23lem25  7950  fin23lem30  7968  domtriomlem  8068  axdc3lem4  8079  axcclem  8083  zorn2lem7  8129  konigthlem  8190  wunr1om  8341  tskr1om  8389  gruen  8434  grur1a  8441  indpi  8531  genpnmax  8631  prlem934  8657  ltaddpr  8658  ltexprlem7  8666  ltaprlem  8668  axrrecex  8785  axpre-sup  8791  lelttr  8912  addid2  8995  fzind  10110  fnn0ind  10111  btwnz  10114  uzwo  10281  uzwoOLD  10282  lbzbi  10306  rpnnen1lem5  10346  xrlelttr  10487  qbtwnre  10526  xrsupsslem  10625  xrinfmsslem  10626  supxrun  10634  fsequb  11037  leexp2r  11159  bernneq  11227  cau3lem  11838  climuni  12026  mulcn2  12069  divalglem8  12599  ndvdssub  12606  rplpwr  12735  algcvgblem  12747  euclemma  12787  prmlem1a  13108  iscatd  13575  plelttr  14106  grpinveu  14516  efgred  15057  lspdisjb  15879  basis2  16689  0ntr  16808  uncmp  17130  1stcrest  17179  txcls  17299  txcnp  17314  tx1stc  17344  fgss2  17569  alexsubALTlem2  17742  alexsubALTlem3  17743  alexsubALTlem4  17744  metcnp3  18086  reconn  18333  iscau4  18705  ellimc3  19229  ulmbdd  19775  ulmcn  19776  sinq12ge0  19876  grpoinveu  20889  gxneg  20933  gxsuc  20939  gxnn0add  20941  gxadd  20942  gxnn0mul  20944  gxmul  20945  ococss  21872  shmodsi  21968  h1datomi  22160  hoaddsub  22396  adjmul  22672  chjatom  22937  atomli  22962  atcvat4i  22977  mdsymlem3  22985  mdsymlem5  22987  mdsymlem6  22988  sumdmdlem  22998  cdj3lem2a  23016  cdj3lem3a  23019  cvmsdisj  23212  eupai  23294  dedekind  23493  fundmpss  23533  dfon2lem6  23555  dfon2lem8  23557  predpoirr  23608  predfrirr  23609  wfr3g  23666  wfrlem12  23678  frr3g  23691  frrlem11  23704  ax5seglem5  23972  ax5seg  23977  ifscgr  24078  lineext  24110  fscgr  24114  idinside  24118  btwnconn1lem11  24131  btwnconn1lem12  24132  btwnconn3  24137  brsegle  24142  seglecgr12  24145  hilbert1.2  24189  areacirc  24343  elioo1t3  24914  iintlem1  25022  clscnc  25422  exp5d  25620  exp5j  25622  exp5k  25623  exp5l  25624  nn0prpwlem  25650  heibor1lem  25945  pridl  26074  pridlc  26108  dmnnzd  26112  prtlem11  26146  prtlem17  26156  isnacs3  26197  jm2.26  26507  sbiota1  27046  stoweidlem17  27178  stoweidlem62  27223  tratrb  27672  onfrALT  27687  in2an  27753  pwtrrVD  27973  pwtrrOLD  27974  suctrALT2VD  27985  suctrALT2  27986  tratrbVD  28010  trintALTVD  28029  trintALT  28030  bnj1204  28415  atcvrj0  28990  cvrat4  29005  athgt  29018  lplnexllnN  29126  2llnjN  29129  lvolnle3at  29144  lncmp  29345  paddclN  29404  pexmidlem4N  29535  cdleme17d3  30058  cdleme50trn2  30113  cdlemf2  30124  cdlemf  30125  cdlemj3  30385  cdlemk26b-3  30467  dihord5b  30822
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