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  1045  nic-ax  1675  nic-axALT  1676  sylgt  1824  axc15  2426  2eu6  2657  reuss2  4266  ssuni  4875  omordi  8501  nnawordi  8557  nnmordi  8567  omabs  8587  omsmolem  8593  unfi  9105  alephordi  9996  dfac5  10051  dfac2a  10052  fin23lem14  10255  facdiv  14249  facwordi  14251  o1lo1  15499  rlimuni  15512  o1co  15548  rlimcn1  15550  rlimcn3  15552  rlimo1  15579  lo1add  15589  lo1mul  15590  rlimno1  15616  caucvgrlem  15635  caucvgrlem2  15637  gcdcllem1  16468  algcvgblem  16546  isprm5  16677  prmfac1  16690  infpnlem1  16881  gsummptnn0fz  19961  gsummoncoe1  22273  evls1fpws  22334  dmatscmcl  22468  decpmatmulsumfsupp  22738  pmatcollpw1lem1  22739  pmatcollpw2lem  22742  pmatcollpwfi  22747  pm2mpmhmlem1  22783  pm2mp  22790  cpmidpmatlem3  22837  cayhamlem4  22853  isclo2  23053  lmcls  23267  isnrm3  23324  dfconn2  23384  1stcrest  23418  dfac14lem  23582  cnpflf2  23965  isucn2  24243  cncfco  24874  ovolicc2lem3  25486  dyadmbllem  25566  itgcn  25812  aalioulem2  26299  aalioulem3  26300  ulmcn  26364  rlimcxp  26937  o1cxp  26938  chtppilimlem2  27437  chtppilim  27438  nosupno  27667  nosupres  27671  noinfno  27682  noinfres  27686  pthdlem1  29834  mdsymlem6  32479  crefss  33993  ss2mcls  35750  mclsax  35751  rdgprc  35974  bj-imim21  36811  bj-axtd  36859  bj-nfimt  36917  bj-nfdt  36993  bj-19.23t  37059  rdgeqoa  37686  rdgssun  37694  wl-cbvmotv  37838  pclclN  40337  primrootscoprbij  42541  isnacs3  43142  syl5imp  44939  imbi12VD  45299  sbcim2gVD  45301  limsupre3lem  46160  limsupub2  46240  fcoresf1  47517  sgoldbeven3prm  48259  ply1mulgsumlem3  48864  ply1mulgsumlem4  48865