Theorem imim1d 75

Description: Deduction adding nested consequents. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 12-Sep-2012.)

Hypothesis

Ref	Expression
imim1d.1

Assertion

Ref	Expression
imim1d

Proof of Theorem imim1d

Step	Hyp	Ref	Expression
1		imim1d.1	. 2
2		idd 24	. 2
3	1, 2	imim12d 74	1

Syntax hints:  ->wi 4

This theorem is referenced by:  imim1  76  expt  156  imbi1d  317  meredith  1472  ax13b  1805  ax12v  1855  sbequi  2116  mo3  2323  morimvOLD  2342  2mo  2373  2moOLD  2374  sstr2  3510  ssralv  3563  soss  4823  frss  4851  fvn0ssdmfun  6022  tfi  6688  nneneq  7720  wemaplem2  7993  unxpwdom2  8035  cantnfp1lem3  8120  cantnfp1lem3OLD  8146  infxpenlem  8412  axpowndlem3  8996  axpowndlem3OLD  8997  indpi  9306  fzind  10987  injresinj  11926  seqcl2  12125  seqfveq2  12129  seqshft2  12133  monoord  12137  seqsplit  12140  seqid2  12153  seqhomo  12154  seqcoll  12512  rexuzre  13185  rexico  13186  limsupbnd2  13306  rlim2lt  13320  rlim3  13321  lo1le  13474  caurcvg  13499  eulerthlem2  14312  ramtlecl  14518  sylow1lem1  16618  efgsrel  16752  elcls3  19584  cncls2  19774  cnntr  19776  filssufilg  20412  ufileu  20420  alexsubALTlem3  20549  tgpt0  20617  isucn2  20782  imasdsf1olem  20876  nmoleub2lem2  21599  ovolicc2lem3  21930  dyadmbllem  22008  dvnres  22334  rlimcnp  23295  xrlimcnp  23298  ftalem2  23347  bcmono  23552  2sqlem6  23644  eupath2  24980  mdslmd1lem1  27244  subfacp1lem6  28629  cvmliftlem7  28736  cvmliftlem10  28739  ss2mcls  28928  mclsax  28929  mettrifi  30250  ply1mulgsumlem1  32986  imbi12VD  33673  bj-exlimh  34211  bj-spimt2  34269  diaintclN  36785  dibintclN  36894  dihintcl  37071  mapdh9a  37517

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7