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

Theorem imim1d 71
Description: Deduction adding nested consequents. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 12-Sep-2012.)
Hypothesis
Ref Expression
imim1d.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
imim1d  |-  ( ph  ->  ( ( ch  ->  th )  ->  ( ps  ->  th ) ) )

Proof of Theorem imim1d
StepHypRef Expression
1 imim1d.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 idd 22 . 2  |-  ( ph  ->  ( th  ->  th )
)
31, 2imim12d 70 1  |-  ( ph  ->  ( ( ch  ->  th )  ->  ( ps  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  imim1  72  expt  150  imbi1d  309  meredith  1413  ax12b  1701  19.23tOLD  1838  ax12olem3OLD  2013  morimv  2328  2mo  2358  sstr2  3347  ssralv  3399  soss  4513  frss  4541  tfi  4825  abianfp  6708  nneneq  7282  wemaplem2  7508  unxpwdom2  7548  cantnfp1lem3  7628  infxpenlem  7887  axpowndlem3  8466  indpi  8776  fzind  10360  injresinj  11192  seqcl2  11333  seqfveq2  11337  seqshft2  11341  monoord  11345  seqsplit  11348  seqid2  11361  seqhomo  11362  seqcoll  11704  rexuzre  12148  rexico  12149  limsupbnd2  12269  rlim2lt  12283  rlim3  12284  lo1le  12437  caurcvg  12462  eulerthlem2  13163  ramtlecl  13360  sylow1lem1  15224  efgsrel  15358  elcls3  17139  cncls2  17329  cnntr  17331  filssufilg  17935  ufileu  17943  alexsubALTlem3  18072  tgpt0  18140  imasdsf1olem  18395  nmoleub2lem2  19116  ovolicc2lem3  19407  dyadmbllem  19483  dvnres  19809  rlimcnp  20796  xrlimcnp  20799  ftalem2  20848  bcmono  21053  2sqlem6  21145  eupath2  21694  mdslmd1lem1  23820  subfacp1lem6  24863  cvmliftlem7  24970  cvmliftlem10  24973  wl-bitr1  26212  mettrifi  26454  imbi12VD  28922  ax12olem3aAUX7  29394  diaintclN  31793  dibintclN  31902  dihintcl  32079  mapdh9a  32525
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator