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  1808  ax12olem3  1882  morimv  2204  2mo  2234  sstr2  3199  ssralv  3250  soss  4348  frss  4376  tfi  4660  abianfp  6487  nneneq  7060  wemaplem2  7278  unxpwdom2  7318  cantnfp1lem3  7398  infxpenlem  7657  axpowndlem3  8237  indpi  8547  fzind  10126  seqcl2  11080  seqfveq2  11084  seqshft2  11088  monoord  11092  seqsplit  11095  seqid2  11108  seqhomo  11109  seqcoll  11417  rexuzre  11852  rexico  11853  limsupbnd2  11973  rlim2lt  11987  rlim3  11988  lo1le  12141  caurcvg  12165  eulerthlem2  12866  ramtlecl  13063  sylow1lem1  14925  efgsrel  15059  elcls3  16836  cncls2  17018  cnntr  17020  filssufilg  17622  ufileu  17630  alexsubALTlem3  17759  tgpt0  17817  imasdsf1olem  17953  nmoleub2lem2  18613  ovolicc2lem3  18894  dyadmbllem  18970  dvnres  19296  rlimcnp  20276  xrlimcnp  20279  ftalem2  20327  bcmono  20532  2sqlem6  20624  mdslmd1lem1  22921  subfacp1lem6  23731  cvmliftlem7  23837  cvmliftlem10  23840  eupath2  23919  wl-bitr1  24982  domrngref  25163  ismonc  25917  icmpmon  25919  isepic  25927  bsstrs  26249  nbssntrs  26250  mettrifi  26576  injresinj  28215  imbi12VD  28965  ax12olem3aAUX7  29434  diaintclN  31870  dibintclN  31979  dihintcl  32156  mapdh9a  32602
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator