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  1060  nic-ax  1703  nic-axALT  1704  sylgt  1852  axc15  2454  2eu6  2684  reuss2  4280  ssuni  4899  omordi  8552  nnawordi  8608  nnmordi  8618  omabs  8638  omsmolem  8644  unfi  9156  alephordi  10059  dfac5  10113  dfac2a  10114  fin23lem14  10318  facdiv  14325  facwordi  14327  o1lo1  15590  rlimuni  15603  o1co  15639  rlimcn1  15641  rlimcn3  15643  rlimo1  15670  lo1add  15680  lo1mul  15681  rlimno1  15707  caucvgrlem  15726  caucvgrlem2  15728  gcdcllem1  16558  algcvgblem  16636  isprm5  16767  prmfac1  16780  infpnlem1  16971  gsummptnn0fz  20057  gsummoncoe1  22449  evls1fpws  22510  dmatscmcl  22641  decpmatmulsumfsupp  22911  pmatcollpw1lem1  22912  pmatcollpw2lem  22915  pmatcollpwfi  22920  pm2mpmhmlem1  22956  pm2mp  22963  cpmidpmatlem3  23010  cayhamlem4  23026  isclo2  23226  lmcls  23440  isnrm3  23497  dfconn2  23557  1stcrest  23591  dfac14lem  23755  cnpflf2  24138  isucn2  24416  cncfco  25047  ovolicc2lem3  25659  dyadmbllem  25739  itgcn  25985  aalioulem2  26477  aalioulem3  26478  ulmcn  26543  rlimcxp  27119  o1cxp  27120  chtppilimlem2  27619  chtppilim  27620  nosupno  27848  nosupres  27852  noinfno  27863  noinfres  27867  pthdlem1  30096  mdsymlem6  32741  crefss  34220  axpowg2  35541  axpowg3  35542  ss2mcls  36041  mclsax  36042  rdgprc  36265  bj-imim21  37120  bj-axtd  37168  bj-nfimt  37226  bj-nfdt  37302  bj-19.23t  37368  rdgeqoa  37997  rdgssun  38005  wl-cbvmotv  38149  pclclN  40646  primrootscoprbij  42850  isnacs3  43424  syl5imp  45204  imbi12VD  45564  sbcim2gVD  45566  limsupre3lem  46429  limsupub2  46509  fcoresf1  47789  sgoldbeven3prm  48531  ply1mulgsumlem3  49151  ply1mulgsumlem4  49152