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  2033  ax11indn  2147  mo  2178  mopick  2218  ralrimivv  2647  mob2  2958  reuind  2981  reupick3  3466  disjiun  4029  sotr2  4359  wefrc  4403  suctr  4491  elpwunsn  4584  dfwe2  4589  limuni3  4659  tfisi  4665  ordom  4681  relop  4850  funcnvuni  5333  fnun  5366  mpteqb  5630  fconst5  5747  funfvima  5769  f1oweALT  5867  frxp  6241  poxp  6243  riotasv3dOLD  6370  onfununi  6374  tfrlem5  6412  tz7.48lem  6469  oecl  6552  oaordex  6572  oaass  6575  omwordri  6586  odi  6593  omass  6594  omeu  6599  oen0  6600  oewordi  6605  oewordri  6606  nnarcl  6630  nnmass  6638  dif1enOLD  7106  dif1en  7107  findcard2  7114  unblem1  7125  unblem2  7126  domunfican  7145  marypha1lem  7202  supiso  7239  inf3lem3  7347  epfrs  7429  karden  7581  infxpenlem  7657  iunfictbso  7757  dfac5  7771  dfac2  7773  kmlem1  7792  kmlem9  7800  infpssrlem3  7947  fin23lem25  7966  fin23lem30  7984  domtriomlem  8084  axdc3lem4  8095  axcclem  8099  zorn2lem7  8145  konigthlem  8206  wunr1om  8357  tskr1om  8405  gruen  8450  grur1a  8457  indpi  8547  genpnmax  8647  prlem934  8673  ltaddpr  8674  ltexprlem7  8682  ltaprlem  8684  axrrecex  8801  axpre-sup  8807  lelttr  8928  addid2  9011  fzind  10126  fnn0ind  10127  btwnz  10130  uzwo  10297  uzwoOLD  10298  lbzbi  10322  rpnnen1lem5  10362  xrlelttr  10503  qbtwnre  10542  xrsupsslem  10641  xrinfmsslem  10642  supxrun  10650  fsequb  11053  leexp2r  11175  bernneq  11243  cau3lem  11854  climuni  12042  mulcn2  12085  divalglem8  12615  ndvdssub  12622  rplpwr  12751  algcvgblem  12763  euclemma  12803  prmlem1a  13124  iscatd  13591  plelttr  14122  grpinveu  14532  efgred  15073  lspdisjb  15895  basis2  16705  0ntr  16824  uncmp  17146  1stcrest  17195  txcls  17315  txcnp  17330  tx1stc  17360  fgss2  17585  alexsubALTlem2  17758  alexsubALTlem3  17759  alexsubALTlem4  17760  metcnp3  18102  reconn  18349  iscau4  18721  ellimc3  19245  ulmbdd  19791  ulmcn  19792  sinq12ge0  19892  grpoinveu  20905  gxneg  20949  gxsuc  20955  gxnn0add  20957  gxadd  20958  gxnn0mul  20960  gxmul  20961  ococss  21888  shmodsi  21984  h1datomi  22176  hoaddsub  22412  adjmul  22688  chjatom  22953  atomli  22978  atcvat4i  22993  mdsymlem3  23001  mdsymlem5  23003  mdsymlem6  23004  sumdmdlem  23014  cdj3lem2a  23032  cdj3lem3a  23035  cvmsdisj  23816  eupai  23898  dedekind  24097  prodmolem2  24158  fundmpss  24193  dfon2lem6  24215  dfon2lem8  24217  predpoirr  24268  predfrirr  24269  wfr3g  24326  wfrlem12  24338  frr3g  24351  frrlem11  24364  ax5seglem5  24633  ax5seg  24638  ifscgr  24739  lineext  24771  fscgr  24775  idinside  24779  btwnconn1lem11  24792  btwnconn1lem12  24793  btwnconn3  24798  brsegle  24803  seglecgr12  24806  hilbert1.2  24850  itg2addnc  25005  areacirc  25034  elioo1t3  25605  iintlem1  25713  clscnc  26113  exp5d  26311  exp5j  26313  exp5k  26314  exp5l  26315  nn0prpwlem  26341  heibor1lem  26636  pridl  26765  pridlc  26799  dmnnzd  26803  prtlem11  26837  prtlem17  26847  isnacs3  26888  jm2.26  27198  sbiota1  27737  stoweidlem17  27869  stoweidlem62  27914  elfznelfzo  28213  tratrb  28598  onfrALT  28613  in2an  28685  pwtrrVD  28916  pwtrrOLD  28917  suctrALT2VD  28928  suctrALT2  28929  tratrbVD  28953  trintALTVD  28972  trintALT  28973  bnj1204  29358  nfsb4twAUX7  29551  nfsb4tOLD7  29699  nfsb4tw2AUXOLD7  29700  atcvrj0  30239  cvrat4  30254  athgt  30267  lplnexllnN  30375  2llnjN  30378  lvolnle3at  30393  lncmp  30594  paddclN  30653  pexmidlem4N  30784  cdleme17d3  31307  cdleme50trn2  31362  cdlemf2  31373  cdlemf  31374  cdlemj3  31634  cdlemk26b-3  31716  dihord5b  32071
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