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  2133  ax11indn  2279  mo  2310  mopick  2350  ralrimivv  2804  mob2  3123  reuind  3146  reupick3  3614  disjiun  4233  sotr2  4567  wefrc  4611  suctrALT  4699  elpwunsn  4792  dfwe2  4797  limuni3  4867  tfisi  4873  ordom  4889  relop  5058  funcnvuni  5553  fnun  5586  mpteqb  5855  fconst5  5985  funfvima  6009  f1oweALT  6110  frxp  6492  poxp  6494  riotasv3dOLD  6635  onfununi  6639  tfrlem5  6677  tz7.48lem  6734  oecl  6817  oaordex  6837  oaass  6840  omwordri  6851  odi  6858  omass  6859  omeu  6864  oen0  6865  oewordi  6870  oewordri  6871  nnarcl  6895  nnmass  6903  dif1enOLD  7376  dif1en  7377  findcard2  7384  unblem1  7395  unblem2  7396  domunfican  7415  marypha1lem  7474  supiso  7513  inf3lem3  7621  epfrs  7703  karden  7857  infxpenlem  7933  iunfictbso  8033  dfac5  8047  dfac2  8049  kmlem1  8068  kmlem9  8076  infpssrlem3  8223  fin23lem25  8242  fin23lem30  8260  domtriomlem  8360  axdc3lem4  8371  axcclem  8375  zorn2lem7  8420  konigthlem  8481  wunr1om  8632  tskr1om  8680  gruen  8725  grur1a  8732  indpi  8822  genpnmax  8922  prlem934  8948  ltaddpr  8949  ltexprlem7  8957  ltaprlem  8959  axrrecex  9076  axpre-sup  9082  lelttr  9203  addid2  9287  fzind  10406  fnn0ind  10407  btwnz  10410  uzwo  10577  uzwoOLD  10578  lbzbi  10602  rpnnen1lem5  10642  xrlelttr  10784  qbtwnre  10823  xrsupsslem  10923  xrinfmsslem  10924  supxrun  10932  elfznelfzo  11230  fsequb  11352  leexp2r  11475  bernneq  11543  brfi1uzind  11753  cau3lem  12196  climuni  12384  mulcn2  12427  divalglem8  12958  ndvdssub  12965  rplpwr  13094  algcvgblem  13106  euclemma  13146  prmlem1a  13467  iscatd  13936  plelttr  14467  grpinveu  14877  efgred  15418  lspdisjb  16236  basis2  17054  0ntr  17173  uncmp  17504  1stcrest  17554  txcls  17674  txcnp  17690  tx1stc  17720  fgss2  17944  alexsubALTlem2  18117  alexsubALTlem3  18118  alexsubALTlem4  18119  metcnp3  18608  reconn  18897  iscau4  19270  ellimc3  19804  ulmbdd  20352  ulmcn  20353  sinq12ge0  20454  eupai  21727  grpoinveu  21848  gxneg  21892  gxsuc  21898  gxnn0add  21900  gxadd  21901  gxnn0mul  21903  gxmul  21904  ococss  22833  shmodsi  22929  h1datomi  23121  hoaddsub  23357  adjmul  23633  chjatom  23898  atomli  23923  atcvat4i  23938  mdsymlem3  23946  mdsymlem5  23948  mdsymlem6  23949  sumdmdlem  23959  cdj3lem2a  23977  cdj3lem3a  23980  cvmsdisj  24992  dedekind  25222  fundmpss  25425  dfon2lem6  25450  dfon2lem8  25452  predpoirr  25507  predfrirr  25508  wfr3g  25572  wfrlem12  25584  frr3g  25616  frrlem11  25629  ax5seglem5  25907  ax5seg  25912  ifscgr  26013  lineext  26045  fscgr  26049  idinside  26053  btwnconn1lem11  26066  btwnconn1lem12  26067  btwnconn3  26072  brsegle  26077  seglecgr12  26080  hilbert1.2  26124  areacirc  26339  exp5d  26345  exp5j  26347  exp5k  26348  exp5l  26349  nn0prpwlem  26367  heibor1lem  26560  pridl  26689  pridlc  26723  dmnnzd  26727  prtlem11  26827  prtlem17  26837  isnacs3  26876  jm2.26  27185  sbiota1  27723  elfzelfzelfz  28230  fzofzim  28257  2ffzoeq  28261  swrdvalodm2  28320  swrdvalodm  28321  swrd0swrd  28329  swrdswrdlem  28330  swrdswrd  28331  swrdccatin1  28337  swrdccatin2  28342  swrdccatin12lem4  28345  swrdccat  28348  2cshw1lem2  28381  2cshwmod  28389  usg2wlkeq  28440  wlkiswwlk2lem3  28473  wlkiswwlk2  28477  wlklniswwlkn2  28480  cusgraisrusgra  28547  frgrancvvdeqlemB  28599  frgrawopreglem5  28609  frg2woteq  28621  tratrb  28792  onfrALT  28807  in2an  28881  pwtrrVD  29112  suctrALT2VD  29122  suctrALT2  29123  tratrbVD  29147  trintALTVD  29166  trintALT  29167  bnj1204  29555  nfsb4twAUX7  29750  nfsb4tOLD7  29919  nfsb4tw2AUXOLD7  29920  atcvrj0  30399  cvrat4  30414  athgt  30427  lplnexllnN  30535  2llnjN  30538  lvolnle3at  30553  lncmp  30754  paddclN  30813  pexmidlem4N  30944  cdleme17d3  31467  cdleme50trn2  31522  cdlemf2  31533  cdlemf  31534  cdlemj3  31794  cdlemk26b-3  31876  dihord5b  32231
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