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

Theorem expdimp 437
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 436 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp 429 1  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  rexlimdvv  2837  ralcom2  2875  reu6  3137  wereu2  4704  ordtr3  4751  oneqmini  4757  suppssrOLD  5825  fun11iun  6526  poxp  6673  suppssr  6709  smoel  6807  omabs  7074  omsmo  7081  iiner  7160  fodomr  7450  fisseneq  7512  suplub2  7699  supnub  7700  inf3lem6  7827  cfcoflem  8429  coftr  8430  zorn2lem7  8659  alephreg  8734  inar1  8929  gruen  8966  letr  9455  lbzbi  10930  xrletr  11119  xmullem  11214  supxrun  11265  ssfzoulel  11604  ssfzo12bi  11605  hashbnd  12092  brfi1uzind  12202  cau3lem  12825  summo  13177  mertenslem2  13327  alzdvds  13565  nn0seqcvgd  13727  divgcdodd  13787  prmpwdvds  13947  catpropd  14630  pltnle  15118  pltval3  15119  pltletr  15123  tsrlemax  15372  frgpnabllem1  16330  cyggexb  16354  abvn0b  17295  isphld  17924  indistopon  18446  restntr  18627  cnprest  18734  lmss  18743  lmmo  18825  2ndcdisj  18901  txlm  19062  flftg  19410  bndth  20371  iscmet3  20645  bcthlem5  20680  ovolicc2lem4  20844  ellimc3  21195  lhop1  21327  ulmcaulem  21743  ulmcau  21744  ulmcn  21748  xrlimcnp  22246  ax5seglem4  23000  axcontlem2  23033  axcontlem4  23035  gxadd  23584  gxmul  23587  nmcvcn  23912  htthlem  24141  atcvat3i  25622  sumdmdlem2  25645  ifeqeqx  25725  prodmolem2  27294  funbreq  27428  sltasym  27659  cgrdegen  27881  lineext  27953  btwnconn1lem7  27970  btwnconn1lem14  27977  waj-ax  28107  lukshef-ax2  28108  fin2solem  28256  unirep  28447  seqpo  28484  ssbnd  28528  intidl  28670  prnc  28708  prtlem15  28862  isnacs3  28888  pm14.24  29528  prmn2uzge3  30092  clwlkisclwwlklem2a  30290  rusgrasn  30400  frgrawopreglem5  30484  extwwlkfablem2  30514  lindslinindsimp1  30697  lindslinindsimp2  30703  bnj23  31406  bnj849  31617  lshpkrlem6  32330  atlatmstc  32534  cvrat3  32656  ps-2  32692  2lplnj  32834  paddasslem5  33038  dochkrshp4  34604
  Copyright terms: Public domain W3C validator