Theorem imim2d 58

Description: Deduction adding nested antecedents. Deduction associated with imim2 59 and imim2i 17. (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 26	. 2 ⊢ (𝜑 → (𝜃 → (𝜓 → 𝜒)))
3	2	a2d 30	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  59  embantd  60  imim12d  82  anc2r  563  dedlem0b  1058  nic-ax  1696  nic-axALT  1697  sylgt  1845  axc15  2456  2eu6  2686  reuss2  4281  ssuni  4894  omordi  8539  nnawordi  8595  nnmordi  8605  omabs  8625  omsmolem  8631  unfi  9143  alephordi  10046  dfac5  10100  dfac2a  10101  fin23lem14  10305  facdiv  14314  facwordi  14316  o1lo1  15578  rlimuni  15591  o1co  15627  rlimcn1  15629  rlimcn3  15631  rlimo1  15658  lo1add  15668  lo1mul  15669  rlimno1  15695  caucvgrlem  15714  caucvgrlem2  15716  gcdcllem1  16547  algcvgblem  16625  isprm5  16756  prmfac1  16769  infpnlem1  16960  gsummptnn0fz  20047  gsummoncoe1  22429  evls1fpws  22490  dmatscmcl  22621  decpmatmulsumfsupp  22891  pmatcollpw1lem1  22892  pmatcollpw2lem  22895  pmatcollpwfi  22900  pm2mpmhmlem1  22936  pm2mp  22943  cpmidpmatlem3  22990  cayhamlem4  23006  isclo2  23206  lmcls  23420  isnrm3  23477  dfconn2  23537  1stcrest  23571  dfac14lem  23735  cnpflf2  24118  isucn2  24396  cncfco  25027  ovolicc2lem3  25639  dyadmbllem  25719  itgcn  25965  aalioulem2  26455  aalioulem3  26456  ulmcn  26520  rlimcxp  27096  o1cxp  27097  chtppilimlem2  27596  chtppilim  27597  nosupno  27825  nosupres  27829  noinfno  27840  noinfres  27844  pthdlem1  30024  mdsymlem6  32669  crefss  34156  axpowg2  35455  axpowg3  35456  ss2mcls  35931  mclsax  35932  rdgprc  36155  bj-imim21  37001  bj-axtd  37049  bj-nfimt  37107  bj-nfdt  37183  bj-19.23t  37249  rdgeqoa  37876  rdgssun  37884  wl-cbvmotv  38028  pclclN  40527  primrootscoprbij  42731  isnacs3  43303  syl5imp  45086  imbi12VD  45446  sbcim2gVD  45448  limsupre3lem  46304  limsupub2  46384  fcoresf1  47661  sgoldbeven3prm  48403  ply1mulgsumlem3  49019  ply1mulgsumlem4  49020