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

Theorem imim1d 69
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 21 . 2  |-  ( ph  ->  ( th  ->  th )
)
31, 2imim12d 68 1  |-  ( ph  ->  ( ( ch  ->  th )  ->  ( ps  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  imim1  70  expt  148  imbi1d  308  meredith  1394  19.23t  1796  ax12olem3  1870  morimv  2191  2mo  2221  sstr2  3186  ssralv  3237  soss  4332  frss  4360  tfi  4644  abianfp  6471  nneneq  7044  wemaplem2  7262  unxpwdom2  7302  cantnfp1lem3  7382  infxpenlem  7641  axpowndlem3  8221  indpi  8531  fzind  10110  seqcl2  11064  seqfveq2  11068  seqshft2  11072  monoord  11076  seqsplit  11079  seqid2  11092  seqhomo  11093  seqcoll  11401  rexuzre  11836  rexico  11837  limsupbnd2  11957  rlim2lt  11971  rlim3  11972  lo1le  12125  caurcvg  12149  eulerthlem2  12850  ramtlecl  13047  sylow1lem1  14909  efgsrel  15043  elcls3  16820  cncls2  17002  cnntr  17004  filssufilg  17606  ufileu  17614  alexsubALTlem3  17743  tgpt0  17801  imasdsf1olem  17937  nmoleub2lem2  18597  ovolicc2lem3  18878  dyadmbllem  18954  dvnres  19280  rlimcnp  20260  xrlimcnp  20263  ftalem2  20311  bcmono  20516  2sqlem6  20608  mdslmd1lem1  22905  subfacp1lem6  23716  cvmliftlem7  23822  cvmliftlem10  23825  eupath2  23904  wl-bitr1  24910  domrngref  25060  ismonc  25814  icmpmon  25816  isepic  25824  bsstrs  26146  nbssntrs  26147  mettrifi  26473  imbi12VD  28649  diaintclN  31248  dibintclN  31357  dihintcl  31534  mapdh9a  31980
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator