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  562  dedlem0b  1055  nic-ax  1692  nic-axALT  1693  sylgt  1841  axc15  2452  2eu6  2682  reuss2  4278  ssuni  4890  omordi  8530  nnawordi  8586  nnmordi  8596  omabs  8616  omsmolem  8622  unfi  9135  alephordi  10027  dfac5  10082  dfac2a  10083  fin23lem14  10287  facdiv  14297  facwordi  14299  o1lo1  15547  rlimuni  15560  o1co  15596  rlimcn1  15598  rlimcn3  15600  rlimo1  15627  lo1add  15637  lo1mul  15638  rlimno1  15664  caucvgrlem  15683  caucvgrlem2  15685  gcdcllem1  16516  algcvgblem  16594  isprm5  16725  prmfac1  16738  infpnlem1  16929  gsummptnn0fz  20009  gsummoncoe1  22351  evls1fpws  22412  dmatscmcl  22543  decpmatmulsumfsupp  22813  pmatcollpw1lem1  22814  pmatcollpw2lem  22817  pmatcollpwfi  22822  pm2mpmhmlem1  22858  pm2mp  22865  cpmidpmatlem3  22912  cayhamlem4  22928  isclo2  23128  lmcls  23342  isnrm3  23399  dfconn2  23459  1stcrest  23493  dfac14lem  23657  cnpflf2  24040  isucn2  24318  cncfco  24949  ovolicc2lem3  25561  dyadmbllem  25641  itgcn  25887  aalioulem2  26374  aalioulem3  26375  ulmcn  26439  rlimcxp  27015  o1cxp  27016  chtppilimlem2  27515  chtppilim  27516  nosupno  27744  nosupres  27748  noinfno  27759  noinfres  27763  pthdlem1  29912  mdsymlem6  32557  crefss  34107  axpowg2  35407  axpowg3  35408  ss2mcls  35882  mclsax  35883  rdgprc  36106  bj-imim21  36953  bj-axtd  37001  bj-nfimt  37059  bj-nfdt  37135  bj-19.23t  37201  rdgeqoa  37828  rdgssun  37836  wl-cbvmotv  37980  pclclN  40479  primrootscoprbij  42683  isnacs3  43255  syl5imp  45052  imbi12VD  45412  sbcim2gVD  45414  limsupre3lem  46270  limsupub2  46350  fcoresf1  47627  sgoldbeven3prm  48369  ply1mulgsumlem3  48974  ply1mulgsumlem4  48975