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

Theorem expd 437
Description: Exportation deduction. (Contributed by NM, 20-Aug-1993.)
Hypothesis
Ref Expression
exp3a.1  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Assertion
Ref Expression
expd  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )

Proof of Theorem expd
StepHypRef Expression
1 exp3a.1 . . . 4  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
21com12 32 . . 3  |-  ( ( ps  /\  ch )  ->  ( ph  ->  th )
)
32ex 435 . 2  |-  ( ps 
->  ( ch  ->  ( ph  ->  th ) ) )
43com3r 82 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  expdimp  438  expcomd  439  expdcom  440  pm3.3  445  syland  483  exp32  608  exp4c  611  exp4d  612  exp42  614  exp44  616  exp5c  619  exp5j  620  impl  624  mpan2d  678  a2and  818  3impib  1203  exp5o  1224  ralrimivv  2843  mob2  3248  reuind  3272  reupick3  3755  elpwunsn  4034  disjiun  4408  sotr2  4795  wefrc  4839  relop  4996  predpoirr  5418  predfrirr  5419  suctr  5516  fnun  5691  mpteqb  5971  tpres  6123  fconst5  6128  funfvima  6146  dfwe2  6613  limuni3  6684  tfisi  6690  ordom  6706  funcnvuni  6751  f1oweALT  6782  frxp  6908  poxp  6910  wfr3g  7033  wfrlem12  7046  onfununi  7059  tz7.48lem  7157  oecl  7238  oaordex  7258  oaass  7261  omwordri  7272  odi  7279  omass  7280  omeu  7285  oen0  7286  oewordi  7291  oewordri  7292  nnarcl  7316  nnmass  7324  dif1en  7801  findcard2  7808  unblem1  7820  unblem2  7821  domunfican  7841  marypha1lem  7944  supiso  7988  inf3lem3  8126  epfrs  8205  karden  8356  infxpenlem  8434  iunfictbso  8534  dfac5  8548  dfac2  8550  kmlem1  8569  kmlem9  8577  infpssrlem3  8724  fin23lem25  8743  fin23lem30  8761  domtriomlem  8861  axdc3lem4  8872  axcclem  8876  zorn2lem7  8921  konigthlem  8982  wunr1om  9133  tskr1om  9181  gruen  9226  grur1a  9233  indpi  9321  genpnmax  9421  prlem934  9447  ltaddpr  9448  ltexprlem7  9456  ltaprlem  9458  axrrecex  9576  axpre-sup  9582  lelttr  9713  dedekind  9786  addid2  9805  nn0lt2  10989  fzind  11022  fnn0ind  11023  btwnz  11026  uzwo  11211  lbzbi  11241  rpnnen1lem5  11283  xrlelttr  11442  qbtwnre  11481  xrsupsslem  11581  xrinfmsslem  11582  supxrun  11590  elfz0ubfz0  11881  elfzo0z  11945  fzofzim  11949  elfznelfzo  12000  fleqceilz  12067  fsequb  12174  leexp2r  12316  bernneq  12384  brfi1uzind  12630  swrdnd2  12763  swrdswrdlem  12789  swrdswrd  12790  wrd2ind  12808  swrdccatin1  12813  swrdccatin2  12817  swrdccatin12lem3  12820  repswswrd  12861  cshweqrep  12894  swrd2lsw  12995  2swrd2eqwrdeq  12996  cau3lem  13385  climuni  13583  mulcn2  13626  divalglem8  14345  ndvdssub  14352  rplpwr  14484  algcvgblem  14496  lcmf  14566  lcmftp  14569  lcmfunsnlem2lem1  14571  lcmfunsnlem2lem2  14572  lcmfdvdsb  14576  lcmfun  14578  euclemma  14625  prmlem1a  15030  iscatd  15523  initoeu1  15850  initoeu2  15855  termoeu1  15857  plelttr  16162  mndclOLD  16491  grpinveu  16644  symgfixelsi  17020  efgred  17326  telgsumfzs  17547  srgmulgass  17692  srgbinom  17706  lspdisjb  18277  mplcoe5lem  18619  cply1mul  18815  coe1fzgsumd  18824  gsummoncoe1  18826  evl1gsumd  18873  cpmatacl  19664  cpmatmcllem  19666  basis2  19890  0ntr  20011  uncmp  20342  1stcrest  20392  txcls  20543  txcnp  20559  tx1stc  20589  fgss2  20813  alexsubALTlem2  20987  alexsubALTlem3  20988  alexsubALTlem4  20989  metcnp3  21479  reconn  21750  iscau4  22135  ellimc3  22708  ulmbdd  23215  ulmcn  23216  sinq12ge0  23325  logblog  23591  ax5seglem5  24806  ax5seg  24811  wlkiswwlk2lem3  25263  wlkiswwlk2  25267  wlklniswwlkn2  25270  usg2wlkeq  25278  wwlknred  25293  wwlknext  25294  wwlkextfun  25299  clwlkisclwwlklem2a4  25354  clwlkisclwwlklem0  25358  wwlksubclwwlk  25374  erclwwlksym  25384  erclwwlknsym  25396  eleclclwwlkn  25403  cusgraisrusgra  25508  rusgranumwlk  25527  eupai  25537  frgrancvvdeqlemB  25608  frgrawopreglem5  25618  frg2woteq  25630  extwwlkfablem2  25648  numclwwlkovf2ex  25656  numclwlk1lem2f1  25664  frgrareggt1  25686  frgrareg  25687  grpoinveu  25792  gxneg  25836  gxsuc  25842  gxnn0add  25844  gxadd  25845  gxnn0mul  25847  gxmul  25848  ococss  26778  shmodsi  26874  h1datomi  27066  hoaddsub  27301  adjmul  27577  chjatom  27842  atomli  27867  atcvat4i  27882  mdsymlem3  27890  mdsymlem5  27892  mdsymlem6  27893  sumdmdlem  27903  cdj3lem2a  27921  cdj3lem3a  27924  bnj1204  29606  cvmsdisj  29778  fundmpss  30191  dfon2lem6  30218  dfon2lem8  30220  frr3g  30297  frrlem11  30310  ifscgr  30593  lineext  30625  fscgr  30629  idinside  30633  btwnconn1lem11  30646  btwnconn1lem12  30647  btwnconn3  30652  brsegle  30657  seglecgr12  30660  hilbert1.2  30704  exp5d  30739  exp5k  30741  exp5l  30742  nn0prpwlem  30760  poimirlem26  31670  poimirlem29  31673  poimirlem32  31676  areacirc  31741  heibor1lem  31845  pridl  31974  pridlc  32008  dmnnzd  32012  prtlem11  32146  prtlem17  32156  ax12indn  32223  atcvrj0  32702  cvrat4  32717  athgt  32730  lplnexllnN  32838  2llnjN  32841  lvolnle3at  32856  lncmp  33057  paddclN  33116  pexmidlem4N  33247  cdleme17d3  33772  cdleme50trn2  33827  cdlemf2  33838  cdlemf  33839  cdlemj3  34099  cdlemk26b-3  34181  dihord5b  34536  isnacs3  35261  jm2.26  35567  sbiota1  36426  exbir  36474  tratrb  36538  onfrALT  36556  in2an  36629  pwtrrVD  36865  suctrALT2VD  36876  suctrALT2  36877  tratrbVD  36902  trintALTVD  36921  trintALT  36922  iccpartiltu  38139  iccpartigtl  38140  iccpartgt  38144  iccpartnel  38155  stgoldbwt  38280  bgoldbst  38282  sgoldbaltlem1  38283  zm1nn  38411  2ffzoeq  38426  lidldomn1  38692  ply1mulgsumlem1  38951  lincsumcl  38997  ellcoellss  39001  islinindfis  39015  lindslinindsimp1  39023  lindslinindsimp2lem5  39028  lindsrng01  39034  elfzolborelfzop1  39090  aacllem  39314
  Copyright terms: Public domain W3C validator