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  1673  nic-axALT  1674  sylgt  1822  axc15  2421  2eu6  2651  reuss2  4292  ssuni  4899  omordi  8533  nnawordi  8588  nnmordi  8598  omabs  8618  omsmolem  8624  unfi  9141  alephordi  10034  dfac5  10089  dfac2a  10090  fin23lem14  10293  facdiv  14259  facwordi  14261  o1lo1  15510  rlimuni  15523  o1co  15559  rlimcn1  15561  rlimcn3  15563  rlimo1  15590  lo1add  15600  lo1mul  15601  rlimno1  15627  caucvgrlem  15646  caucvgrlem2  15648  gcdcllem1  16476  algcvgblem  16554  isprm5  16684  prmfac1  16697  infpnlem1  16888  gsummptnn0fz  19923  gsummoncoe1  22202  evls1fpws  22263  dmatscmcl  22397  decpmatmulsumfsupp  22667  pmatcollpw1lem1  22668  pmatcollpw2lem  22671  pmatcollpwfi  22676  pm2mpmhmlem1  22712  pm2mp  22719  cpmidpmatlem3  22766  cayhamlem4  22782  isclo2  22982  lmcls  23196  isnrm3  23253  dfconn2  23313  1stcrest  23347  dfac14lem  23511  cnpflf2  23894  isucn2  24173  cncfco  24807  ovolicc2lem3  25427  dyadmbllem  25507  itgcn  25753  aalioulem2  26248  aalioulem3  26249  ulmcn  26315  rlimcxp  26891  o1cxp  26892  chtppilimlem2  27392  chtppilim  27393  nosupno  27622  nosupres  27626  noinfno  27637  noinfres  27641  pthdlem1  29703  mdsymlem6  32344  crefss  33846  ss2mcls  35562  mclsax  35563  rdgprc  35789  bj-imim21  36546  bj-axtd  36589  bj-nfimt  36633  bj-nfdt  36691  bj-19.23t  36765  bj-19.36im  36766  rdgeqoa  37365  rdgssun  37373  wl-cbvmotv  37508  pclclN  39892  primrootscoprbij  42097  isnacs3  42705  syl5imp  44509  imbi12VD  44869  sbcim2gVD  44871  limsupre3lem  45737  limsupub2  45817  fcoresf1  47074  sgoldbeven3prm  47788  ply1mulgsumlem3  48381  ply1mulgsumlem4  48382