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  2426  2eu6  2657  reuss2  4278  ssuni  4888  omordi  8493  nnawordi  8549  nnmordi  8559  omabs  8579  omsmolem  8585  unfi  9095  alephordi  9984  dfac5  10039  dfac2a  10040  fin23lem14  10243  facdiv  14210  facwordi  14212  o1lo1  15460  rlimuni  15473  o1co  15509  rlimcn1  15511  rlimcn3  15513  rlimo1  15540  lo1add  15550  lo1mul  15551  rlimno1  15577  caucvgrlem  15596  caucvgrlem2  15598  gcdcllem1  16426  algcvgblem  16504  isprm5  16634  prmfac1  16647  infpnlem1  16838  gsummptnn0fz  19915  gsummoncoe1  22252  evls1fpws  22313  dmatscmcl  22447  decpmatmulsumfsupp  22717  pmatcollpw1lem1  22718  pmatcollpw2lem  22721  pmatcollpwfi  22726  pm2mpmhmlem1  22762  pm2mp  22769  cpmidpmatlem3  22816  cayhamlem4  22832  isclo2  23032  lmcls  23246  isnrm3  23303  dfconn2  23363  1stcrest  23397  dfac14lem  23561  cnpflf2  23944  isucn2  24222  cncfco  24856  ovolicc2lem3  25476  dyadmbllem  25556  itgcn  25802  aalioulem2  26297  aalioulem3  26298  ulmcn  26364  rlimcxp  26940  o1cxp  26941  chtppilimlem2  27441  chtppilim  27442  nosupno  27671  nosupres  27675  noinfno  27686  noinfres  27690  pthdlem1  29839  mdsymlem6  32483  crefss  34006  ss2mcls  35762  mclsax  35763  rdgprc  35986  bj-imim21  36751  bj-axtd  36794  bj-nfimt  36838  bj-nfdt  36897  bj-19.23t  36971  bj-19.36im  36972  rdgeqoa  37571  rdgssun  37579  wl-cbvmotv  37714  pclclN  40147  primrootscoprbij  42352  isnacs3  42948  syl5imp  44749  imbi12VD  45109  sbcim2gVD  45111  limsupre3lem  45972  limsupub2  46052  fcoresf1  47311  sgoldbeven3prm  48025  ply1mulgsumlem3  48630  ply1mulgsumlem4  48631