Theorem imim2d 57

Description: Deduction adding nested antecedents. Deduction associated with imim2 58 and imim2i 16. (Contributed by NM, 10-Jan-1993.)

Hypothesis

Ref	Expression
imim2d.1	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
imim2d	|- ( ph -> ( ( th -> ps ) -> ( th -> ch ) ) )

Proof of Theorem imim2d

Step	Hyp	Ref	Expression
1		imim2d.1	. . 3 |- ( ph -> ( ps -> ch ) )
2	1	a1d 25	. 2 |- ( ph -> ( th -> ( ps -> ch ) ) )
3	2	a2d 29	1 |- ( ph -> ( ( th -> ps ) -> ( th -> ch ) ) )

Syntax hints:   -> wi 4

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

This theorem is referenced by:  imim2  58  embantd  59  imim12d  81  anc2r  579  pm5.31  612  dedlem0b  1001  nic-ax  1598  nic-axALT  1599  sylgt  1749  nfimt  1821  nfimdOLD  2226  2eu6  2558  reuss2  3907  ssuni  4459  ssuniOLD  4460  omordi  7646  nnawordi  7701  nnmordi  7711  omabs  7727  omsmolem  7733  alephordi  8897  dfac5  8951  dfac2a  8952  fin23lem14  9155  facdiv  13074  facwordi  13076  o1lo1  14268  rlimuni  14281  o1co  14317  rlimcn1  14319  rlimcn2  14321  rlimo1  14347  lo1add  14357  lo1mul  14358  rlimno1  14384  caucvgrlem  14403  caucvgrlem2  14405  gcdcllem1  15221  algcvgblem  15290  isprm5  15419  prmfac1  15431  infpnlem1  15614  gsummptnn0fz  18382  gsummoncoe1  19674  dmatscmcl  20309  decpmatmulsumfsupp  20578  pmatcollpw1lem1  20579  pmatcollpw2lem  20582  pmatcollpwfi  20587  pm2mpmhmlem1  20623  pm2mp  20630  cpmidpmatlem3  20677  cayhamlem4  20693  isclo2  20892  lmcls  21106  isnrm3  21163  dfconn2  21222  1stcrest  21256  dfac14lem  21420  cnpflf2  21804  isucn2  22083  cncfco  22710  ovolicc2lem3  23287  dyadmbllem  23367  itgcn  23609  aalioulem2  24088  aalioulem3  24089  ulmcn  24153  rlimcxp  24700  o1cxp  24701  chtppilimlem2  25163  chtppilim  25164  pthdlem1  26662  mdsymlem6  29267  crefss  29916  ss2mcls  31465  mclsax  31466  rdgprc  31700  nosupno  31849  nosupres  31853  bj-imim21  32539  bj-axtd  32578  bj-ssbim  32621  bj-nfdt  32686  rdgeqoa  33218  pm5.31r  34143  pclclN  35177  isnacs3  37273  syl5imp  38718  imbi12VD  39109  sbcim2gVD  39111  limsupre3lem  39964  sgoldbeven3prm  41671  ply1mulgsumlem3  42176  ply1mulgsumlem4  42177