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

Theorem expdimp 428
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 427 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp 420 1  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  rexlimdvv  2838  ralcom2  2874  reu6  3125  wereu2  4581  ordtr3  4628  oneqmini  4634  fun11iun  5697  suppssr  5866  poxp  6460  smoel  6624  omabs  6892  omsmo  6899  iiner  6978  fodomr  7260  fisseneq  7322  suplub2  7468  supnub  7469  inf3lem6  7590  cfcoflem  8154  coftr  8155  zorn2lem7  8384  alephreg  8459  inar1  8652  gruen  8689  letr  9169  lbzbi  10566  xrletr  10750  xmullem  10845  supxrun  10896  hashbnd  11626  brfi1uzind  11717  cau3lem  12160  summo  12513  mertenslem2  12664  alzdvds  12901  nn0seqcvgd  13063  divgcdodd  13121  prmpwdvds  13274  catpropd  13937  pltnle  14425  pltval3  14426  pltletr  14430  tsrlemax  14654  frgpnabllem1  15486  cyggexb  15510  abvn0b  16364  isphld  16887  indistopon  17067  restntr  17248  cnprest  17355  lmss  17364  lmmo  17446  2ndcdisj  17521  txlm  17682  flftg  18030  bndth  18985  iscmet3  19248  bcthlem5  19283  ovolicc2lem4  19418  ellimc3  19768  lhop1  19900  ulmcaulem  20312  ulmcau  20313  ulmcn  20317  xrlimcnp  20809  gxadd  21865  gxmul  21868  nmcvcn  22193  htthlem  22422  atcvat3i  23901  sumdmdlem2  23924  ifeqeqx  24003  prodmolem2  25263  funbreq  25397  sltasym  25629  ax5seglem4  25873  axcontlem2  25906  axcontlem4  25908  cgrdegen  25940  lineext  26012  btwnconn1lem7  26029  btwnconn1lem14  26036  waj-ax  26166  lukshef-ax2  26167  unirep  26416  seqpo  26453  ssbnd  26499  intidl  26641  prnc  26679  prtlem15  26726  isnacs3  26766  pm14.24  27611  swrdvalodmlem1  28209  frgrawopreglem5  28499  bnj23  29145  bnj849  29358  lshpkrlem6  29975  atlatmstc  30179  cvrat3  30301  ps-2  30337  2lplnj  30479  paddasslem5  30683  dochkrshp4  32249
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 179  df-an 362
  Copyright terms: Public domain W3C validator