MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imim1d 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  1410  ax12b  1697  19.23tOLD  1834  ax12olem3OLD  1979  morimv  2302  2mo  2332  sstr2  3315  ssralv  3367  soss  4481  frss  4509  tfi  4792  abianfp  6675  nneneq  7249  wemaplem2  7472  unxpwdom2  7512  cantnfp1lem3  7592  infxpenlem  7851  axpowndlem3  8430  indpi  8740  fzind  10324  injresinj  11155  seqcl2  11296  seqfveq2  11300  seqshft2  11304  monoord  11308  seqsplit  11311  seqid2  11324  seqhomo  11325  seqcoll  11667  rexuzre  12111  rexico  12112  limsupbnd2  12232  rlim2lt  12246  rlim3  12247  lo1le  12400  caurcvg  12425  eulerthlem2  13126  ramtlecl  13323  sylow1lem1  15187  efgsrel  15321  elcls3  17102  cncls2  17291  cnntr  17293  filssufilg  17896  ufileu  17904  alexsubALTlem3  18033  tgpt0  18101  imasdsf1olem  18356  nmoleub2lem2  19077  ovolicc2lem3  19368  dyadmbllem  19444  dvnres  19770  rlimcnp  20757  xrlimcnp  20760  ftalem2  20809  bcmono  21014  2sqlem6  21106  eupath2  21655  mdslmd1lem1  23781  subfacp1lem6  24824  cvmliftlem7  24931  cvmliftlem10  24934  wl-bitr1  26124  mettrifi  26353  imbi12VD  28694  ax12olem3aAUX7  29163  diaintclN  31541  dibintclN  31650  dihintcl  31827  mapdh9a  32273
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator