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  1671  nic-axALT  1672  sylgt  1820  axc15  2430  2eu6  2660  reuss2  4345  ssuni  4956  omordi  8622  nnawordi  8677  nnmordi  8687  omabs  8707  omsmolem  8713  unfi  9238  alephordi  10143  dfac5  10198  dfac2a  10199  fin23lem14  10402  facdiv  14336  facwordi  14338  o1lo1  15583  rlimuni  15596  o1co  15632  rlimcn1  15634  rlimcn3  15636  rlimo1  15663  lo1add  15673  lo1mul  15674  rlimno1  15702  caucvgrlem  15721  caucvgrlem2  15723  gcdcllem1  16545  algcvgblem  16624  isprm5  16754  prmfac1  16767  infpnlem1  16957  gsummptnn0fz  20028  gsummoncoe1  22333  evls1fpws  22394  dmatscmcl  22530  decpmatmulsumfsupp  22800  pmatcollpw1lem1  22801  pmatcollpw2lem  22804  pmatcollpwfi  22809  pm2mpmhmlem1  22845  pm2mp  22852  cpmidpmatlem3  22899  cayhamlem4  22915  isclo2  23117  lmcls  23331  isnrm3  23388  dfconn2  23448  1stcrest  23482  dfac14lem  23646  cnpflf2  24029  isucn2  24309  cncfco  24952  ovolicc2lem3  25573  dyadmbllem  25653  itgcn  25900  aalioulem2  26393  aalioulem3  26394  ulmcn  26460  rlimcxp  27035  o1cxp  27036  chtppilimlem2  27536  chtppilim  27537  nosupno  27766  nosupres  27770  noinfno  27781  noinfres  27785  pthdlem1  29802  mdsymlem6  32440  crefss  33795  ss2mcls  35536  mclsax  35537  rdgprc  35758  bj-imim21  36517  bj-axtd  36560  bj-nfimt  36604  bj-nfdt  36662  bj-19.23t  36736  bj-19.36im  36737  rdgeqoa  37336  rdgssun  37344  wl-cbvmotv  37467  pclclN  39848  primrootscoprbij  42059  isnacs3  42666  syl5imp  44483  imbi12VD  44844  sbcim2gVD  44846  limsupre3lem  45653  limsupub2  45733  fcoresf1  46984  sgoldbeven3prm  47657  ply1mulgsumlem3  48117  ply1mulgsumlem4  48118