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  2673  ralcom2  2704  reu6  2954  wereu2  4390  ordtr3  4437  oneqmini  4443  fun11iun  5493  suppssr  5659  poxp  6227  smoel  6377  omabs  6645  omsmo  6652  iiner  6731  fodomr  7012  fisseneq  7074  suplub2  7212  supnub  7213  inf3lem6  7334  cfcoflem  7898  coftr  7899  zorn2lem7  8129  alephreg  8204  inar1  8397  gruen  8434  letr  8914  lbzbi  10306  xrletr  10489  xmullem  10584  supxrun  10634  hashbnd  11343  cau3lem  11838  summo  12190  mertenslem2  12341  alzdvds  12578  nn0seqcvgd  12740  divgcdodd  12798  prmpwdvds  12951  catpropd  13612  pltnle  14100  pltval3  14101  pltletr  14105  tsrlemax  14329  frgpnabllem1  15161  cyggexb  15185  abvn0b  16043  isphld  16558  indistopon  16738  restntr  16912  cnprest  17017  lmss  17026  lmmo  17108  2ndcdisj  17182  txlm  17342  flftg  17691  bndth  18456  iscmet3  18719  bcthlem5  18750  ovolicc2lem4  18879  ellimc3  19229  lhop1  19361  ulmcaulem  19771  ulmcau  19772  ulmcn  19776  xrlimcnp  20263  gxadd  20942  gxmul  20945  nmcvcn  21268  htthlem  21497  atcvat3i  22976  sumdmdlem2  22999  funbreq  24127  sltasym  24326  ax5seglem4  24560  axcontlem2  24593  axcontlem4  24595  cgrdegen  24627  lineext  24699  btwnconn1lem7  24716  btwnconn1lem14  24723  waj-ax  24853  lukshef-ax2  24854  fldi  25427  qusp  25542  unirep  26349  seqpo  26457  ssbnd  26512  intidl  26654  prnc  26692  prtlem15  26743  isnacs3  26785  pm14.24  27632  rfcnnnub  27707  bnj23  28744  bnj849  28957  lshpkrlem6  29305  atlatmstc  29509  cvrat3  29631  ps-2  29667  2lplnj  29809  paddasslem5  30013  dochkrshp4  31579
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