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

Theorem expdimp 426
Description: A deduction version of exportation, followed by importation. (Contributed by NM, 6-Sep-2008.)
Hypothesis
Ref Expression
exp3a.1  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Assertion
Ref Expression
expdimp  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)

Proof of Theorem expdimp
StepHypRef Expression
1 exp3a.1 . . 3  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
21exp3a 425 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp 418 1  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  rexlimdvv  2686  ralcom2  2717  reu6  2967  wereu2  4406  ordtr3  4453  oneqmini  4459  fun11iun  5509  suppssr  5675  poxp  6243  smoel  6393  omabs  6661  omsmo  6668  iiner  6747  fodomr  7028  fisseneq  7090  suplub2  7228  supnub  7229  inf3lem6  7350  cfcoflem  7914  coftr  7915  zorn2lem7  8145  alephreg  8220  inar1  8413  gruen  8450  letr  8930  lbzbi  10322  xrletr  10505  xmullem  10600  supxrun  10650  hashbnd  11359  cau3lem  11854  summo  12206  mertenslem2  12357  alzdvds  12594  nn0seqcvgd  12756  divgcdodd  12814  prmpwdvds  12967  catpropd  13628  pltnle  14116  pltval3  14117  pltletr  14121  tsrlemax  14345  frgpnabllem1  15177  cyggexb  15201  abvn0b  16059  isphld  16574  indistopon  16754  restntr  16928  cnprest  17033  lmss  17042  lmmo  17124  2ndcdisj  17198  txlm  17358  flftg  17707  bndth  18472  iscmet3  18735  bcthlem5  18766  ovolicc2lem4  18895  ellimc3  19245  lhop1  19377  ulmcaulem  19787  ulmcau  19788  ulmcn  19792  xrlimcnp  20279  gxadd  20958  gxmul  20961  nmcvcn  21284  htthlem  21513  atcvat3i  22992  sumdmdlem2  23015  funbreq  24198  sltasym  24397  ax5seglem4  24632  axcontlem2  24665  axcontlem4  24667  cgrdegen  24699  lineext  24771  btwnconn1lem7  24788  btwnconn1lem14  24795  waj-ax  24925  lukshef-ax2  24926  fldi  25530  qusp  25645  unirep  26452  seqpo  26560  ssbnd  26615  intidl  26757  prnc  26795  prtlem15  26846  isnacs3  26888  pm14.24  27735  rfcnnnub  27810  bnj23  29060  bnj849  29273  lshpkrlem6  29927  atlatmstc  30131  cvrat3  30253  ps-2  30289  2lplnj  30431  paddasslem5  30635  dochkrshp4  32201
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