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	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
imim2d	⊢ (𝜑 → ((𝜃 → 𝜓) → (𝜃 → 𝜒)))

Proof of Theorem imim2d

Step	Hyp	Ref	Expression
1		imim2d.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	a1d 25	. 2 ⊢ (𝜑 → (𝜃 → (𝜓 → 𝜒)))
3	2	a2d 29	1 ⊢ (𝜑 → ((𝜃 → 𝜓) → (𝜃 → 𝜒)))

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  554  dedlem0b  1044  nic-ax  1674  nic-axALT  1675  sylgt  1823  axc15  2422  2eu6  2652  reuss2  4276  ssuni  4884  omordi  8481  nnawordi  8536  nnmordi  8546  omabs  8566  omsmolem  8572  unfi  9080  alephordi  9962  dfac5  10017  dfac2a  10018  fin23lem14  10221  facdiv  14191  facwordi  14193  o1lo1  15441  rlimuni  15454  o1co  15490  rlimcn1  15492  rlimcn3  15494  rlimo1  15521  lo1add  15531  lo1mul  15532  rlimno1  15558  caucvgrlem  15577  caucvgrlem2  15579  gcdcllem1  16407  algcvgblem  16485  isprm5  16615  prmfac1  16628  infpnlem1  16819  gsummptnn0fz  19896  gsummoncoe1  22221  evls1fpws  22282  dmatscmcl  22416  decpmatmulsumfsupp  22686  pmatcollpw1lem1  22687  pmatcollpw2lem  22690  pmatcollpwfi  22695  pm2mpmhmlem1  22731  pm2mp  22738  cpmidpmatlem3  22785  cayhamlem4  22801  isclo2  23001  lmcls  23215  isnrm3  23272  dfconn2  23332  1stcrest  23366  dfac14lem  23530  cnpflf2  23913  isucn2  24191  cncfco  24825  ovolicc2lem3  25445  dyadmbllem  25525  itgcn  25771  aalioulem2  26266  aalioulem3  26267  ulmcn  26333  rlimcxp  26909  o1cxp  26910  chtppilimlem2  27410  chtppilim  27411  nosupno  27640  nosupres  27644  noinfno  27655  noinfres  27659  pthdlem1  29742  mdsymlem6  32383  crefss  33857  ss2mcls  35600  mclsax  35601  rdgprc  35827  bj-imim21  36584  bj-axtd  36627  bj-nfimt  36671  bj-nfdt  36729  bj-19.23t  36803  bj-19.36im  36804  rdgeqoa  37403  rdgssun  37411  wl-cbvmotv  37546  pclclN  39929  primrootscoprbij  42134  isnacs3  42742  syl5imp  44544  imbi12VD  44904  sbcim2gVD  44906  limsupre3lem  45769  limsupub2  45849  fcoresf1  47099  sgoldbeven3prm  47813  ply1mulgsumlem3  48419  ply1mulgsumlem4  48420