Theorem imim2d 52

Description: Deduction adding nested antecedents. (Contributed by NM, 10-Jan-1993.)

Hypothesis

Ref	Expression
imim2d.1

Assertion

Ref	Expression
imim2d

Proof of Theorem imim2d

Step	Hyp	Ref	Expression
1		imim2d.1	. . 3
2	1	a1d 25	. 2
3	2	a2d 26	1

Syntax hints:  ->wi 4

This theorem is referenced by:  imim2  53  embantd  54  imim12d  74  anc2r  556  pm5.31  588  ornldOLD  899  dedlem0b  953  nic-ax  1506  nic-axALT  1507  19.23t  1909  nfimd  1917  2eu6  2383  ssuni  4271  omordi  7234  nnawordi  7289  nnmordi  7299  omabs  7315  omsmolem  7321  alephordi  8476  dfac5  8530  dfac2a  8531  fin23lem14  8734  facdiv  12365  facwordi  12367  o1lo1  13360  rlimuni  13373  o1co  13409  rlimcn1  13411  rlimcn2  13413  rlimo1  13439  lo1add  13449  lo1mul  13450  rlimno1  13476  caucvgrlem  13495  caucvgrlem2  13497  gcdcllem1  14149  algcvgblem  14206  isprm5  14253  prmfac1  14259  infpnlem1  14428  gsummptnn0fz  17014  gsummoncoe1  18346  dmatscmcl  19005  decpmatmulsumfsupp  19274  pmatcollpw1lem1  19275  pmatcollpw2lem  19278  pmatcollpwfi  19283  pm2mpmhmlem1  19319  pm2mp  19326  cpmidpmatlem3  19373  cayhamlem4  19389  isclo2  19589  lmcls  19803  isnrm3  19860  dfcon2  19920  1stcrest  19954  dfac14lem  20118  cnpflf2  20501  isucn2  20782  cncfco  21411  ovolicc2lem3  21930  dyadmbllem  22008  itgcn  22249  aalioulem2  22729  aalioulem3  22730  ulmcn  22794  rlimcxp  23303  o1cxp  23304  chtppilimlem2  23659  chtppilim  23660  frgrancvvdgeq  25043  mdsymlem6  27327  crefss  27852  ss2mcls  28928  mclsax  28929  rdgprc  29227  pm5.31r  30594  isnacs3  30642  ply1mulgsumlem3  32988  ply1mulgsumlem4  32989  syl5imp  33282  imbi12VD  33673  sbcim2gVD  33675  bj-axtd  34182  bj-alrimh  34208  bj-nfdt  34249  pclclN  35615

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